Encyclopedia Cost Cost Uniqueness T5 Uniqueness Complete

ARTICLE 3 claims 3 theorems

Cost Uniqueness T5 Uniqueness Complete

A single function describes the cost of recognition, and the framework proves no other function can do the job.

Verify this page

The uniqueness theorem

The cost of recognition is the price a system pays for registering a change in scale. In the Recognition Science framework, this cost is not a free choice. The central theorem, T5_uniqueness_complete, proves that any cost function satisfying five plain conditions must equal the function J(x) = (x + 1/x)/2 - 1 for every positive x. The conditions are: symmetry under swapping x and 1/x, zero cost at x = 1, strict convexity, a calibration condition, and a composition law. The theorem is machine-checked in the framework's library of formal theorems, meaning the proof has been verified step by step by a computer.

The composition law deserves a closer look. It says that the cost of recognizing a product xy can be expressed in terms of the costs of recognizing x and y separately, through a specific algebraic identity. In symbols, the law forces F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y). This is not an assumption about physics; it is a structural requirement on any cost function. The theorem shows that this law, together with the other four conditions, pins down J exactly. Without the composition law, many other functions would satisfy the remaining conditions. The regularity hypotheses, which include continuity and smoothness, rule out pathological solutions that would otherwise exist.

The proof does not rely on any special axioms beyond the standard logical foundations. The framework's library states that the theorem uses no framework-specific axioms; the ingredients are supplied as explicit hypotheses. This means the result is conditional: if a cost function meets the stated conditions, then it must equal J. The theorem does not claim that any particular physical process actually uses this cost. It establishes a mathematical uniqueness result, not an empirical measurement.

What the theorem does not claim is just as important. It does not claim that the cost function J is the only possible cost in every conceivable universe; it only claims uniqueness within the class of functions satisfying the five conditions. It does not claim that the composition law itself is derived from more basic principles; the law is an explicit hypothesis. And it does not claim that the framework's other results, such as the golden ratio or the eight-tick cycle, follow from this theorem alone. Those results build on this uniqueness, but they require additional steps in the forcing chain.

For the reader, the practical consequence is this: if you accept the five conditions as reasonable requirements for a cost of recognition, then the form of that cost is forced. There is no room for alternative models within this framework. The theorem turns a philosophical question about the nature of recognition into a precise mathematical statement, and it does so with a proof that a computer has checked.

THEOREM T5_uniqueness_complete · IndisputableMonolith/CostUniqueness.lean
T5_uniqueness_complete · IndisputableMonolith/CostUniqueness.lean:26 
/-- Full T5 Uniqueness Theorem (with explicit functional-identity hypothesis) -/
theorem T5_uniqueness_complete (F : ℝ → ℝ)
  (hSymm : ∀ {x}, 0 < x → F x = F x⁻¹)
  (hUnit : F 1 = 0)
  (hConvex : StrictConvexOn ℝ (Set.Ioi 0) F)
  (hCalib : deriv (deriv (F ∘ exp)) 0 = 1)
  (hCont : ContinuousOn F (Ioi 0))
  (hCoshAdd : FunctionalEquation.CoshAddIdentity F)
  (h_smooth_hyp : FunctionalEquation.dAlembert_continuous_implies_smooth_hypothesis (FunctionalEquation.H F))
  (h_ode_hyp : FunctionalEquation.dAlembert_to_ODE_hypothesis (FunctionalEquation.H F))
  (h_cont_hyp : FunctionalEquation.ode_regularity_continuous_hypothesis (FunctionalEquation.H F))
  (h_diff_hyp : FunctionalEquation.ode_regularity_differentiable_hypothesis (FunctionalEquation.H F))
  (h_bootstrap_hyp : FunctionalEquation.ode_linear_regularity_bootstrap_hypothesis (FunctionalEquation.H F)) :
  ∀ {x : ℝ}, 0 < x → F x = Jcost x := by
  intro x hx
  -- Reduce to log coordinates and invoke d'Alembert uniqueness
  let Gf : ℝ → ℝ := FunctionalEquation.G F
  have h_even : Function.Even Gf := FunctionalEquation.G_even_of_reciprocal_symmetry F hSymm
  have h_G0 : Gf 0 = 0 := FunctionalEquation.G_zero_of_unit F hUnit

  -- Gf is continuous on ℝ (F is continuous on (0,∞), exp is continuous, composition is continuous)
  have h_G_cont : Continuous Gf := by
    have h := ContinuousOn.comp_continuous hCont continuous_exp
    have h' : Continuous (fun t => F (Real.exp t)) :=
      h (by intro t; exact mem_Ioi.mpr (Real.exp_pos t))
    simpa [FunctionalEquation.G] using h'

  -- Convert CoshAddIdentity F to DirectCoshAdd Gf
  have h_direct : FunctionalEquation.DirectCoshAdd Gf :=
    FunctionalEquation.CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd

  -- Apply d'Alembert uniqueness (via the shifted H := G + 1) to get Gf(t) = cosh(t) - 1.
  let Hf : ℝ → ℝ := FunctionalEquation.H F
  have h_H0 : Hf 0 = 1 := by
    simp [Hf, FunctionalEquation.H, FunctionalEquation.G, hUnit]
  have h_H_cont : Continuous Hf := by
    simpa [Hf, FunctionalEquation.H] using h_G_cont.add continuous_const
  have h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u := by
    intro t u
    have hG := h_direct t u
    -- Convert the direct cosh-add identity for G into the d'Alembert identity for H := G + 1.
    -- This is pure ring algebra.
    -- (G(t+u)+G(t-u)) = 2(Gt·Gu) + 2(Gt+Gu)
    -- ⇔ (H(t+u)+H(t-u)) = 2HtHu  for H := G + 1.
    have h_goal :
        (Gf (t + u) + 1) + (Gf (t - u) + 1) = 2 * (Gf t + 1) * (Gf u + 1) := by
      calc
        (Gf (t + u) + 1) + (Gf (t - u) + 1)
            = (Gf (t + u) + Gf (t - u)) + 2 := by ring
        _ = (2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)) + 2 := by simpa [hG]
        _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
    -- Discharge the original goal by unfolding Hf := H F := G F + 1 and rewriting in terms of Gf.
    simpa [Hf, FunctionalEquation.H, Gf] using h_goal
  have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
    -- Hf = Gf + 1, so the 2nd derivative at 0 is the same as for Gf.
    have hG_d2 : deriv (deriv Gf) 0 = 1 := by
      simpa [Gf, FunctionalEquation.G] using hCalib
    -- `deriv (Hf)` equals `deriv (Gf)` pointwise, so their second derivatives match too.
    have hderiv : deriv Hf = deriv Gf := by
      funext t
      -- Unfold Hf := (fun y => Gf y + 1), then apply `deriv_add_const`.
      change deriv (fun y => Gf y + 1) t = deriv Gf t
      simpa using (deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ)))
    have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
    have hderiv2_at0 : deriv (deriv Hf) 0 = deriv (deriv Gf) 0 := congrArg (fun g => g 0) hderiv2
    exact hderiv2_at0.trans hG_d2
  have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
    FunctionalEquation.dAlembert_cosh_solution
      Hf h_H0 h_H_cont h_dAlembert h_H_d2 h_smooth_hyp h_ode_hyp h_cont_hyp h_diff_hyp h_bootstrap_hyp
  have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := by
    intro t
    have hH := h_H_cosh t
    -- Unshift: H = G + 1.
    have hH' : Gf t + 1 = Real.cosh t := by
      simpa [Hf, FunctionalEquation.H, Gf] using hH
    linarith

  -- Now convert back using the log-parametrization identity for Jcost
  have ht : Real.exp (Real.log x) = x := Real.exp_log hx
  have hJG : FunctionalEquation.G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
    FunctionalEquation.Jcost_G_eq_cosh_sub_one (Real.log x)
  calc F x
      = F (Real.exp (Real.log x)) := by rw [ht]
    _ = Gf (Real.log x) := rfl
    _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
    _ = FunctionalEquation.G Cost.Jcost (Real.log x) := by simpa using hJG.symm
    _ = Jcost (Real.exp (Real.log x)) := by simp [FunctionalEquation.G]
    _ = Jcost x := by simpa [ht]
THEOREM Jcost_satisfies_composition_law · IndisputableMonolith/CostUniqueness.lean
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
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 the composition law is derived from more basic principles; it is an explicit hypothesis. The theorem does not claim that any physical system actually uses this cost function. The theorem does not claim that the golden ratio or eight-tick cycle follow from this theorem alone.

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