Encyclopedia Foundation Foundation Cost Axioms Uniqueness Specification

ARTICLE 4 claims 4 theorems

Foundation Cost Axioms Uniqueness Specification

Three plain conditions on a cost function force it to be exactly J(x) = (x + 1/x)/2 - 1, no exceptions.

Verify this page

The uniqueness theorem

The declaration uniqueness_specification proves a uniqueness theorem for a cost function. A cost function here is a rule that assigns a number to every positive ratio x, measuring how expensive that ratio is relative to unity. The theorem states that if such a function satisfies three primitive axioms, plus a set of regularity conditions, then it must equal J(x) = (x + x⁻¹)/2 - 1 for every positive x. The three axioms are: normalization, meaning F(1) = 0, so unity costs nothing; a composition law, F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y), which forces multiplicative consistency; and calibration, fixing the second derivative at 1. The regularity conditions are continuity and strict convexity on the positive reals, together with smoothness hypotheses drawn from Aczél's theorem on d'Alembert equations.

The theorem is proved in the machine-checked library of formal theorems. It is a theorem, not a definition: it derives the form of J from the axioms, rather than choosing J by hand. The proof proceeds through a chain of lemmas. First, composition and normalization together imply symmetry, so F(x) = F(x⁻¹). Then the d'Alembert equation is transformed into a differential equation, and the regularity hypotheses allow a bootstrap that yields the closed form. The result is that the cost of being at ratio x is (x + 1/x)/2 - 1, which is zero exactly at x = 1, grows quadratically as x moves away from 1, and tends to infinity as x approaches 0.

In Recognition Science, this uniqueness result is the foundation of the framework. It shows that the cost function is forced, not chosen: any cost function satisfying the plain conditions must be J. The theorem also yields an existence criterion: for positive x, the statement "x exists" is equivalent to x = 1, because J(x) = 0 only at x = 1. And it yields the meta-principle that nothing costs infinity, since J(x) is unbounded near zero. These consequences are derived, not assumed.

What the theorem does not claim is equally important. It does not claim that the axioms are true of the physical world; that is a modeling choice, not a mathematical result. It does not claim that any particular physical system actually has this cost function. And it does not claim that the regularity conditions are unnecessary: without continuity, convexity, and the smoothness hypotheses, the d'Alembert equation admits pathological solutions, so the uniqueness depends on those conditions. The theorem is a conditional statement: if the axioms and regularity hold, then the form is forced.

THEOREM uniqueness_specification · IndisputableMonolith/Foundation/CostAxioms.lean
uniqueness_specification · IndisputableMonolith/Foundation/CostAxioms.lean:317 
/-- **T5 Uniqueness (Specification)**:
    Any function F satisfying the three cost axioms with regularity equals J.

    This is the central uniqueness theorem of Recognition Science.
    The complete proof is in CostUniqueness.lean via T5_uniqueness_complete.

    The proof structure is:
    1. CostFunctionalAxioms.composition gives d'Alembert: F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)
    2. Substituting G(t) = F(exp(t)) transforms to cosh-additive: G(s+t) + G(s-t) = 2G(s)G(t) + 2G(s) + 2G(t)
    3. Shifting H = G + 1 gives standard d'Alembert: H(s+t) + H(s-t) = 2H(s)H(t)
    4. The unique continuous solution is H(t) = cosh(t), so G(t) = cosh(t) - 1
    5. Therefore F(x) = cosh(log(x)) - 1 = ½(x + x⁻¹) - 1 = J(x)

    The regularity hypotheses (Aczél theory for d'Alembert equations) are stated
    explicitly. These are standard results from functional equation theory:
    - Continuous d'Alembert solutions are smooth (Aczél 1966)
    - Smooth d'Alembert solutions satisfy ODE H'' = H
    - Linear ODE regularity bootstrap

    See `IndisputableMonolith.T5_uniqueness_complete` for the rigorous proof. -/
theorem uniqueness_specification (F : ℝ → ℝ) [CostFunctionalAxioms F]
    (hCont : ContinuousOn F (Set.Ioi 0))
    (hConvex : StrictConvexOn ℝ (Set.Ioi 0) F)
    -- Regularity hypotheses from Aczél's theorem on d'Alembert equations
    (h_smooth : Cost.FunctionalEquation.dAlembert_continuous_implies_smooth_hypothesis
        (Cost.FunctionalEquation.H F))
    (h_ode : Cost.FunctionalEquation.dAlembert_to_ODE_hypothesis
        (Cost.FunctionalEquation.H F))
    (h_cont : Cost.FunctionalEquation.ode_regularity_continuous_hypothesis
        (Cost.FunctionalEquation.H F))
    (h_diff : Cost.FunctionalEquation.ode_regularity_differentiable_hypothesis
        (Cost.FunctionalEquation.H F))
    (h_boot : Cost.FunctionalEquation.ode_linear_regularity_bootstrap_hypothesis
        (Cost.FunctionalEquation.H F)) :
    ∀ x, 0 < x → F x = J x := by
  intro x hx
  -- Bridge from CostFunctionalAxioms to T5_uniqueness_complete hypotheses
  -- 1. Symmetry: F(x) = F(1/x)
  have hSymm : ∀ {x : ℝ}, 0 < x → F x = F x⁻¹ :=
    Composition_Normalization_implies_symmetry F
  -- 2. Unit normalization: F(1) = 0
  have hUnit : F 1 = 0 := Normalization.unit_zero
  -- 3. Calibration: deriv (deriv (F ∘ exp)) 0 = 1
  have hCalib : deriv (deriv (F ∘ exp)) 0 = 1 := Calibration.second_deriv_at_zero
  -- 4. CoshAddIdentity: from Composition axiom
  have hCoshAdd : Cost.FunctionalEquation.CoshAddIdentity F :=
    Composition_implies_CoshAddIdentity F
  -- Apply T5_uniqueness_complete with all hypotheses
  unfold J
  exact CostUniqueness.T5_uniqueness_complete F hSymm hUnit hConvex hCalib hCont hCoshAdd
    h_smooth h_ode h_cont h_diff h_boot hx
THEOREM Composition_Normalization_implies_symmetry · IndisputableMonolith/Foundation/CostAxioms.lean
Composition_Normalization_implies_symmetry · IndisputableMonolith/Foundation/CostAxioms.lean:292 
/-- Composition + Normalization implies symmetry: F(x) = F(1/x).

    Proof: Apply Composition with x = 1:
    F(1 * y) + F(1 / y) = 2F(1)F(y) + 2F(1) + 2F(y)
    F(y) + F(1/y) = 2 * 0 * F(y) + 2 * 0 + 2F(y)  (by Normalization: F(1) = 0)
    F(y) + F(1/y) = 2F(y)
    F(1/y) = F(y)

    Therefore F(y) = F(1/y) for all y > 0, which is symmetry. -/
theorem Composition_Normalization_implies_symmetry (F : ℝ → ℝ) [Composition F] [Normalization F] :
    ∀ {x : ℝ}, 0 < x → F x = F x⁻¹ := by
  intro x hx
  -- Apply Composition with x = 1, y = x
  have h := Composition.dAlembert (F := F) 1 x one_pos hx
  -- F(1 * x) + F(1 / x) = 2F(1)F(x) + 2F(1) + 2F(x)
  -- Simplify: F(1) = 0, 1 * x = x, 1 / x = x⁻¹
  simp only [one_mul, one_div, Normalization.unit_zero, zero_mul, add_zero, mul_zero] at h
  -- h is now: F(x) + F(x⁻¹) = 2F(x)
  -- Subtracting F(x) from both sides: F(x⁻¹) = F(x)
  have h_symm : F x⁻¹ = F x := by
    have h_sub : F x⁻¹ = (F x + F x⁻¹) - F x := by ring
    rw [h_sub, h]
    ring
  exact h_symm.symm
THEOREM unity_is_unique_existent · IndisputableMonolith/Foundation/CostAxioms.lean
unity_is_unique_existent · IndisputableMonolith/Foundation/CostAxioms.lean:235 
/-- Unity is the unique existent. -/
theorem unity_is_unique_existent : ∀ x : ℝ, Exists x ↔ x = 1 := by
  intro x
  by_cases hx : 0 < x
  · exact law_of_existence hx
  · simp only [Exists]
    constructor
    · intro ⟨hpos, _⟩; exact absurd hpos hx
    · intro heq; subst heq; exact ⟨one_pos, by simp [J]⟩
THEOREM nothing_costs_infinity · IndisputableMonolith/Foundation/CostAxioms.lean
nothing_costs_infinity · IndisputableMonolith/Foundation/CostAxioms.lean:258 
/-- Alternative formulation: No finite-cost state can approach Nothing. -/
theorem nothing_costs_infinity :
    ¬∃ C : ℝ, ∀ x, 0 < x → J x ≤ C := by
  push_neg
  intro C
  obtain ⟨ε, hε, hJ⟩ := J_arbitrarily_large_near_zero C
  use ε / 2
  constructor
  · linarith
  · exact hJ (ε / 2) (by linarith) (by linarith)

What this page does not claim

The axioms are true of the physical world; that is a modeling choice. Any particular physical system actually has J as its cost function. The uniqueness holds without the regularity conditions; the d'Alembert equation alone admits other solutions.

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/Foundation/CostAxioms.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