Encyclopedia Foundation Foundation Cost Axioms Composition Implies Cosh Add Identity

ARTICLE 3 claims 3 theorems

Foundation Cost Axioms Composition Implies Cosh Add Identity

One equation governs how recognition costs combine, and it forces a specific symmetric form on any cost function that obeys it.

Verify this page

The composition law

The d'Alembert functional equation is a classical object in mathematics, studied since the 18th century. It asks for functions F that satisfy F(x+y) + F(x−y) = 2F(x)F(y), a condition that forces solutions to be trigonometric or hyperbolic functions. In the Recognition Science framework, a variant of this equation appears as a primitive axiom about how the cost of recognition, the price a system pays for registering a ratio between two quantities, combines across scales.

The framework's composition axiom states that for any positive x and y, F(x·y) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y). This is not the classical d'Alembert form, but a shifted version adapted to the framework's normalization F(1) = 0. The declaration Composition_implies_CoshAddIdentity proves, within the machine-checked library of formal theorems, that any function satisfying this composition law also satisfies a hyperbolic cosine addition identity: F(x·y) + F(x/y) = 2F(x)F(y) + 2. This is a purely algebraic consequence of the composition axiom alone; it requires no assumptions about continuity, differentiability, or any other regularity condition.

The result matters because it separates what the composition law forces from what it does not. The composition axiom alone pins down the algebraic structure of the cost function: it must behave like a hyperbolic cosine under multiplication and division. But the composition law does not by itself select the specific function J(x) = (x + 1/x)/2 − 1. That uniqueness requires two additional axioms, normalization and calibration, plus regularity hypotheses drawn from Aczél's theorem on d'Alembert equations. The theorem Composition_implies_CoshAddIdentity is a stepping stone, not the final uniqueness result.

In the framework's account, this algebraic consequence supports the later derivation that the unique cost function is J(x) = (x + 1/x)/2 − 1, a result that then forces the golden ratio as a self-similar scaling and, further down the chain, an eight-tick recognition cycle and three spatial dimensions. The composition law is the first link in that chain, and this theorem shows exactly how much structure that single link already carries.

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 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 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

What this page does not claim

The composition axiom alone forces the unique cost function J(x) = (x + 1/x)/2 − 1. The declaration proves the full uniqueness theorem without additional regularity hypotheses. The hyperbolic cosine addition identity is the same as the classical d'Alembert equation.

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