Encyclopedia Cost Cost Functional Equation Composition Log Curvature Forces Jcost

ARTICLE 2 claims 2 theorems

Cost Functional Equation Composition Log Curvature Forces Jcost

A single equation governs the unavoidable cost of recognition, and a machine-checked proof forces the result exactly.

Verify this page

The forced cost function

The cost function is a mathematical object that assigns a number to every positive real input. In the Recognition Science framework, this number represents the cost of a recognition event, a discrete record of something happening. The central question is whether the cost is forced to take one specific form, or whether many different forms are possible.

The classical answer comes from functional equations. A functional equation is an equation where the unknown is a function, not a number. The relevant one here is a composition law, which relates the cost of a product to the costs of its factors. The law states that for all positive x and y, F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y). This is not an arbitrary choice; it is the condition that the cost of combining two recognitions is determined by the costs of the individual recognitions.

In 1747, Jean le Rond d'Alembert studied a similar equation, H(t+u) + H(t-u) = 2H(t)H(u), which arises in the theory of vibrating strings. Its continuous solutions are exactly the hyperbolic cosine, H(t) = cosh(t). The Recognition Science framework reuses this classical result. By changing variables, the composition law becomes a d'Alembert equation for a related function. The framework then adds a regularity condition called log-curvature, which fixes the scale of the solution. The theorem composition_logCurvature_forces_jcost states that any function satisfying the composition law and having log-curvature 1 must equal the cost function J(x) = (x + 1/x)/2 - 1 for all positive x.

This is a strong uniqueness result. It says that the cost function is not a free choice. Once the composition law and the log-curvature condition are accepted, the form of the cost is forced. The proof is carried out in a machine-checked library of formal theorems, meaning every step is verified by a computer. The theorem is part of a chain that leads to the golden ratio, the number of ticks in a recognition cycle, and the number of spatial dimensions.

What this theorem does not claim is equally important. It does not claim that the composition law or the log-curvature condition are derived from first principles. Those are premises, definitional choices that the framework makes. The theorem only shows that given those premises, the conclusion follows. It also does not claim that the cost function J is the only function satisfying the composition law without the log-curvature condition. Without that condition, other solutions exist. The theorem is a conditional statement, not an unconditional one.

In Recognition Science, the significance is that a single, simple equation governs the cost of recognition. This is not a metaphor; it is a mathematical fact with a machine-checked proof. The result provides a foundation for the framework's other claims, such as the emergence of the golden ratio and the number of spatial dimensions. For a reader, the takeaway is that the cost function is not arbitrary. It is a specific, unique object, forced by a small set of conditions.

THEOREM composition_logCurvature_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean
composition_logCurvature_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean:1301 
/-- **The cost theorem on two premises.** The composition law and unit log
curvature force `F = J` on the positives. Normalization, nonnegativity, and
continuity are all conclusions rather than hypotheses; compare
`law_of_logic_forces_jcost`, which assumes all of them. -/
theorem composition_logCurvature_forces_jcost [AczelSmoothnessPackage]
    (F : ℝ → ℝ)
    (hComp : SatisfiesCompositionLaw F)
    (hκ : HasLogCurvature (H F) 1) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  have hNorm : IsNormalized F := logCurvature_forces_normalized F hComp hκ
  have hN : F 1 = 0 := hNorm
  have hH0 : H F 0 = 1 := by simp [H, G, hN]
  have hCosh : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
  have hdA : ∀ t u, H F (t + u) + H F (t - u) = 2 * H F t * H F u := by
    intro t u
    have hG := hCosh t u
    have hgoal :
        (G F (t + u) + 1) + (G F (t - u) + 1) =
          2 * (G F t + 1) * (G F u + 1) := by
      calc
        (G F (t + u) + 1) + (G F (t - u) + 1)
            = (G F (t + u) + G F (t - u)) + 2 := by ring
        _ = (2 * (G F t * G F u) + 2 * (G F t + G F u)) + 2 := by simpa [hG]
        _ = 2 * (G F t + 1) * (G F u + 1) := by ring
    simpa [H] using hgoal
  have hcont : Continuous (H F) :=
    dAlembert_continuous_of_log_curvature (H F) hH0 hdA hκ
  have hsm : ContDiff ℝ ⊤ (H F) := aczel_dAlembert_smooth (H F) hH0 hcont hdA
  have heven : Function.Even (H F) := dAlembert_even (H F) hH0 hdA
  have hd0 : deriv (H F) 0 = 0 :=
    even_deriv_at_zero (H F) heven
      (hsm.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) 0)
  have hd2 : deriv (deriv (H F)) 0 = 1 :=
    deriv2_of_logCurvature (H F) hsm hH0 hd0 hκ
  have hcosh : ∀ t, H F t = Real.cosh t :=
    dAlembert_cosh_solution_aczel (H F) hH0 hcont hdA hd2
  intro x hx
  have hGc : G F (Real.log x) = Real.cosh (Real.log x) - 1 := by
    have h := hcosh (Real.log x)
    simp only [H] at h
    linarith
  have ht : Real.exp (Real.log x) = x := Real.exp_log hx
  have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
    Jcost_G_eq_cosh_sub_one (Real.log x)
  calc
    F x = F (Real.exp (Real.log x)) := by rw [ht]
    _ = G F (Real.log x) := rfl
    _ = Real.cosh (Real.log x) - 1 := hGc
    _ = G Cost.Jcost (Real.log x) := by simp only [hJG]
    _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
    _ = Cost.Jcost x := by simp [ht]
THEOREM composition_logCurvature_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean
composition_logCurvature_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean:1301 
/-- **The cost theorem on two premises.** The composition law and unit log
curvature force `F = J` on the positives. Normalization, nonnegativity, and
continuity are all conclusions rather than hypotheses; compare
`law_of_logic_forces_jcost`, which assumes all of them. -/
theorem composition_logCurvature_forces_jcost [AczelSmoothnessPackage]
    (F : ℝ → ℝ)
    (hComp : SatisfiesCompositionLaw F)
    (hκ : HasLogCurvature (H F) 1) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  have hNorm : IsNormalized F := logCurvature_forces_normalized F hComp hκ
  have hN : F 1 = 0 := hNorm
  have hH0 : H F 0 = 1 := by simp [H, G, hN]
  have hCosh : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
  have hdA : ∀ t u, H F (t + u) + H F (t - u) = 2 * H F t * H F u := by
    intro t u
    have hG := hCosh t u
    have hgoal :
        (G F (t + u) + 1) + (G F (t - u) + 1) =
          2 * (G F t + 1) * (G F u + 1) := by
      calc
        (G F (t + u) + 1) + (G F (t - u) + 1)
            = (G F (t + u) + G F (t - u)) + 2 := by ring
        _ = (2 * (G F t * G F u) + 2 * (G F t + G F u)) + 2 := by simpa [hG]
        _ = 2 * (G F t + 1) * (G F u + 1) := by ring
    simpa [H] using hgoal
  have hcont : Continuous (H F) :=
    dAlembert_continuous_of_log_curvature (H F) hH0 hdA hκ
  have hsm : ContDiff ℝ ⊤ (H F) := aczel_dAlembert_smooth (H F) hH0 hcont hdA
  have heven : Function.Even (H F) := dAlembert_even (H F) hH0 hdA
  have hd0 : deriv (H F) 0 = 0 :=
    even_deriv_at_zero (H F) heven
      (hsm.differentiable (by decide : (⊤ : WithTop ℕ∞) ≠ 0) 0)
  have hd2 : deriv (deriv (H F)) 0 = 1 :=
    deriv2_of_logCurvature (H F) hsm hH0 hd0 hκ
  have hcosh : ∀ t, H F t = Real.cosh t :=
    dAlembert_cosh_solution_aczel (H F) hH0 hcont hdA hd2
  intro x hx
  have hGc : G F (Real.log x) = Real.cosh (Real.log x) - 1 := by
    have h := hcosh (Real.log x)
    simp only [H] at h
    linarith
  have ht : Real.exp (Real.log x) = x := Real.exp_log hx
  have hJG : G Cost.Jcost (Real.log x) = Real.cosh (Real.log x) - 1 :=
    Jcost_G_eq_cosh_sub_one (Real.log x)
  calc
    F x = F (Real.exp (Real.log x)) := by rw [ht]
    _ = G F (Real.log x) := rfl
    _ = Real.cosh (Real.log x) - 1 := hGc
    _ = G Cost.Jcost (Real.log x) := by simp only [hJG]
    _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
    _ = Cost.Jcost x := by simp [ht]

What this page does not claim

The composition law and log-curvature condition are derived from first principles. The cost function J is the only function satisfying the composition law without the log-curvature condition. The theorem proves the existence of recognition events or the physical reality of the framework.

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/Cost/FunctionalEquation.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