Encyclopedia Cost Cost Uniqueness Unique Cost On Pos From Rcl

ARTICLE 3 claims 3 theorems

Cost Uniqueness Unique Cost On Pos From Rcl

A single cost function for recognition is forced by five plain conditions, a result proved in a machine-checked library of formal theorems.

Verify this page

The uniqueness theorem

The cost function J(x) = (x + 1/x)/2 - 1 is the unique function on positive numbers that satisfies five plain conditions: reciprocal symmetry (cost is unchanged when x is replaced by 1/x), zero cost at unity, a forced composition law, calibration, and continuity. This is a proved theorem in the framework's machine-checked library of formal theorems, not a conjecture or a model choice. The declaration unique_cost_on_pos_from_rcl states it directly: any cost functional F meeting those conditions must equal Jcost on (0, ∞).

The conditions are not arbitrary. Reciprocal symmetry says the cost of recognizing a ratio is the same as recognizing its reciprocal. Zero cost at unity means recognizing the trivial ratio costs nothing. The composition law ties the cost of a product to the costs of its factors. Calibration fixes the scale of the cost in log coordinates, and continuity rules out pathological jumps. Together they force the single formula J(x) = (x + 1/x)/2 - 1, which is strictly convex on positive numbers and satisfies all the conditions itself.

The theorem is axiom-clean in the sense that it avoids global axioms; the functional-equation ingredients are supplied as explicit hypotheses in the theorem statement. This means the result is conditional on those hypotheses, not on an unstated background assumption. The proof combines results from convexity, calibration, and functional equations, and the declaration Jcost_is_reciprocal, Jcost_is_normalized, Jcost_satisfies_composition_law, and Jcost_is_calibrated verify that Jcost itself meets each condition.

What the theorem does not claim is as important as what it proves. It does not claim that any real-world process must obey these conditions; that is a modeling question. It does not claim the conditions are the only possible ones, nor that the cost function is unique without the composition law or calibration. The theorem is a mathematical implication: if the conditions hold, the cost is forced. Whether recognition in nature satisfies them is a separate question, left open by this declaration.

The practical consequence is that the framework's entire cost structure reduces to a single function, and the golden ratio, the eight-tick cycle, and three spatial dimensions follow from it in the forcing chain. But that chain is not part of this theorem; it lives in separate declarations. This page establishes the uniqueness of Jcost on positive numbers, nothing more and nothing less.

THEOREM unique_cost_on_pos_from_rcl · IndisputableMonolith/CostUniqueness.lean
unique_cost_on_pos_from_rcl · IndisputableMonolith/CostUniqueness.lean:161 
/-- Axiom-free uniqueness theorem on the paper's RCL theorem surface.

This is the main unconditional IM-facing T5 statement: the caller supplies
the reciprocal, normalization, composition, calibration, continuity, and
explicit d'Alembert regularity hypotheses, and the conclusion is `F = Jcost`
on `(0, ∞)`. -/
theorem unique_cost_on_pos_from_rcl (F : ℝ → ℝ)
    (hRecip : FunctionalEquation.IsReciprocalCost F)
    (hNorm : FunctionalEquation.IsNormalized F)
    (hComp : FunctionalEquation.SatisfiesCompositionLaw F)
    (hCalib : FunctionalEquation.IsCalibrated F)
    (hCont : ContinuousOn F (Ioi 0))
    (h_smooth : FunctionalEquation.dAlembert_continuous_implies_smooth_hypothesis (FunctionalEquation.H F))
    (h_ode : FunctionalEquation.dAlembert_to_ODE_hypothesis (FunctionalEquation.H F))
    (h_cont : FunctionalEquation.ode_regularity_continuous_hypothesis (FunctionalEquation.H F))
    (h_diff : FunctionalEquation.ode_regularity_differentiable_hypothesis (FunctionalEquation.H F))
    (h_boot : FunctionalEquation.ode_linear_regularity_bootstrap_hypothesis (FunctionalEquation.H F)) :
    ∀ {x : ℝ}, 0 < x → F x = Jcost x := by
  intro x hx
  exact FunctionalEquation.law_of_logic_forces_jcost_with_regularization F
    hRecip hNorm hComp hCalib hCont h_smooth h_ode h_cont h_diff h_boot x hx

/- Jcost satisfies the non-axiomatic hypothesis bundle (unused here)
 def Jcost_satisfies_axioms : UniqueCostAxioms Jcost where
  symmetric := fun hx => Jcost_symm hx
  unit := Jcost_unit0
  convex := Jcost_strictConvexOn_pos
  calibrated := by
    simpa using IndisputableMonolith.CPM.LawOfExistence.RS.Jcost_log_second_deriv_normalized
  continuousOn_pos := Jcost_continuous_pos
  coshAdd := FunctionalEquation.Jcost_cosh_add_identity -/
THEOREM Jcost_is_reciprocal · Jcost_is_normalized · Jcost_satisfies_composition_law · Jcost_is_calibrated · IndisputableMonolith/CostUniqueness.lean
Jcost_is_reciprocal · IndisputableMonolith/CostUniqueness.lean:144 
/-- `Jcost` satisfies reciprocal symmetry in the theorem-surface format. -/
theorem Jcost_is_reciprocal : FunctionalEquation.IsReciprocalCost Jcost :=
  fun x hx => Jcost_symm hx
Jcost_is_normalized · IndisputableMonolith/CostUniqueness.lean:148 
/-- `Jcost` is normalized at `1`. -/
theorem Jcost_is_normalized : FunctionalEquation.IsNormalized Jcost :=
  Jcost_unit0
Jcost_satisfies_composition_law · IndisputableMonolith/CostUniqueness.lean:152 
/-- `Jcost` satisfies the Recognition Composition Law. -/
theorem Jcost_satisfies_composition_law : FunctionalEquation.SatisfiesCompositionLaw Jcost :=
  (FunctionalEquation.composition_law_equiv_coshAdd Jcost).2 FunctionalEquation.Jcost_cosh_add_identity
Jcost_is_calibrated · IndisputableMonolith/CostUniqueness.lean:156 
/-- `Jcost` satisfies the standard calibration condition in log coordinates. -/
theorem Jcost_is_calibrated : FunctionalEquation.IsCalibrated Jcost := by
  change deriv (deriv (fun t : ℝ => Jcost (Real.exp t))) 0 = 1
  exact IndisputableMonolith.CPM.LawOfExistence.RS.Jcost_log_second_deriv_normalized
THEOREM unique_cost_on_pos_from_rcl · IndisputableMonolith/CostUniqueness.lean
unique_cost_on_pos_from_rcl · IndisputableMonolith/CostUniqueness.lean:161 
/-- Axiom-free uniqueness theorem on the paper's RCL theorem surface.

This is the main unconditional IM-facing T5 statement: the caller supplies
the reciprocal, normalization, composition, calibration, continuity, and
explicit d'Alembert regularity hypotheses, and the conclusion is `F = Jcost`
on `(0, ∞)`. -/
theorem unique_cost_on_pos_from_rcl (F : ℝ → ℝ)
    (hRecip : FunctionalEquation.IsReciprocalCost F)
    (hNorm : FunctionalEquation.IsNormalized F)
    (hComp : FunctionalEquation.SatisfiesCompositionLaw F)
    (hCalib : FunctionalEquation.IsCalibrated F)
    (hCont : ContinuousOn F (Ioi 0))
    (h_smooth : FunctionalEquation.dAlembert_continuous_implies_smooth_hypothesis (FunctionalEquation.H F))
    (h_ode : FunctionalEquation.dAlembert_to_ODE_hypothesis (FunctionalEquation.H F))
    (h_cont : FunctionalEquation.ode_regularity_continuous_hypothesis (FunctionalEquation.H F))
    (h_diff : FunctionalEquation.ode_regularity_differentiable_hypothesis (FunctionalEquation.H F))
    (h_boot : FunctionalEquation.ode_linear_regularity_bootstrap_hypothesis (FunctionalEquation.H F)) :
    ∀ {x : ℝ}, 0 < x → F x = Jcost x := by
  intro x hx
  exact FunctionalEquation.law_of_logic_forces_jcost_with_regularization F
    hRecip hNorm hComp hCalib hCont h_smooth h_ode h_cont h_diff h_boot x hx

/- Jcost satisfies the non-axiomatic hypothesis bundle (unused here)
 def Jcost_satisfies_axioms : UniqueCostAxioms Jcost where
  symmetric := fun hx => Jcost_symm hx
  unit := Jcost_unit0
  convex := Jcost_strictConvexOn_pos
  calibrated := by
    simpa using IndisputableMonolith.CPM.LawOfExistence.RS.Jcost_log_second_deriv_normalized
  continuousOn_pos := Jcost_continuous_pos
  coshAdd := FunctionalEquation.Jcost_cosh_add_identity -/

What this page does not claim

The theorem does not claim that any real-world process must satisfy the five conditions; that is a modeling question. The theorem does not claim uniqueness without the composition law or calibration. The theorem does not claim the forcing chain from Jcost to three spatial dimensions; that is proved in separate declarations.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/CostUniqueness.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND