Encyclopedia Foundation Foundation Cost Axioms

ARTICLE 5 claims 5 theorems

Foundation Cost Axioms

Three plain conditions on a cost function force a single formula, and from that formula the framework derives the rest of its structure.

Verify this page

The cost axioms

A cost function assigns a number to each possible state of a system, measuring how far that state is from a preferred one. In the Recognition Science framework, the preferred state is called unity, and the cost of being at unity is set to zero. The framework's foundation cost axioms are three conditions that any such cost function must satisfy. The first, normalization, says the cost at unity is exactly zero. The second, recognition composition, is a consistency rule: the cost of a product of two ratios plus the cost of their quotient must equal a specific combination of the individual costs. The third, calibration, fixes the scale by requiring the second derivative of the cost, measured in logarithmic units, to equal one at unity.

These three axioms are not arbitrary. They encode an economic inevitability: approaching nothingness costs infinity, while consistency costs little. The framework proves that any function satisfying all three conditions must equal J(x) = (x + 1/x)/2 - 1. This uniqueness result is a theorem in the machine-checked library of formal theorems, with no unproved assumptions. The formula has a striking property: it is symmetric, meaning J(x) = J(1/x), so a ratio and its reciprocal carry the same cost. It is also always nonnegative for positive x, reaching zero only at x = 1, the point of perfect balance.

In Recognition Science, the axioms are more primitive than logic itself. The framework defines existence as having zero cost: a state exists exactly when its cost is zero, which the theorem shows happens only at unity. The framework also derives a meta-principle from the axioms: nothing cannot recognize itself, because the cost of approaching zero grows without bound. This principle, tagged as a theorem, follows from the fact that J(x) tends to infinity as x tends to zero.

The axioms were chosen to be as plain as possible. Normalization and calibration are simple scaling choices. The composition rule is the substantive one: it forces multiplicative consistency across all ratios. The framework proves that this rule, together with the other two, implies a hyperbolic cosine addition identity, which is the key step in deriving the unique form of J. The regularity conditions needed for the uniqueness proof, such as continuity and convexity, are stated explicitly in the theorem, and the framework's library shows that J itself satisfies all the axioms.

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 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)
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 Composition_implies_CoshAddIdentity · IndisputableMonolith/Foundation/CostAxioms.lean
Composition_implies_CoshAddIdentity · IndisputableMonolith/Foundation/CostAxioms.lean:271 
/-- Composition axiom implies CoshAddIdentity in log coordinates. -/
theorem Composition_implies_CoshAddIdentity (F : ℝ → ℝ) [Composition F] :
    Cost.FunctionalEquation.CoshAddIdentity F := by
  intro t u
  -- G F (t+u) + G F (t-u) = F(exp(t+u)) + F(exp(t-u))
  -- = F(exp(t) * exp(u)) + F(exp(t) / exp(u))
  -- = 2 * F(exp(t)) * F(exp(u)) + 2 * F(exp(t)) + 2 * F(exp(u))  (by Composition)
  -- = 2 * (G F t * G F u) + 2 * (G F t + G F u)
  simp only [Cost.FunctionalEquation.G]
  have hpos_t : 0 < Real.exp t := Real.exp_pos t
  have hpos_u : 0 < Real.exp u := Real.exp_pos u
  have h1 : Real.exp (t + u) = Real.exp t * Real.exp u := Real.exp_add t u
  have h2 : Real.exp (t - u) = Real.exp t / Real.exp u := by
    rw [sub_eq_add_neg, Real.exp_add, Real.exp_neg]
    ring
  rw [h1, h2]
  have h_dAlembert := Composition.dAlembert (F := F) (Real.exp t) (Real.exp u) hpos_t hpos_u
  -- The RHS needs regrouping: 2 * F x * F y + 2 * F x + 2 * F y = 2 * (F x * F y) + 2 * (F x + F y)
  convert h_dAlembert using 1
  ring
THEOREM J_symmetric · IndisputableMonolith/Foundation/CostAxioms.lean
J_symmetric · IndisputableMonolith/Foundation/CostAxioms.lean:137 
/-- J is symmetric: J(x) = J(1/x) for positive x. -/
theorem J_symmetric {x : ℝ} (hx : 0 < x) : J x = J x⁻¹ := by
  have hx0 : x ≠ 0 := hx.ne'
  simp only [J]
  field_simp
  ring

What this page does not claim

The cost axioms alone do not force the fine-structure constant alpha. The framework does not prove the Riemann Hypothesis; it only shows an equivalence with an RS-structural statement. The uniqueness theorem requires explicit regularity hypotheses such as continuity and convexity, not just the three axioms.

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