Encyclopedia Cost Cost Cont Diff Reduction

ARTICLE 3 claims 3 theorems

Cost Cont Diff Reduction

A classic functional equation, solved with just two derivatives instead of a stack of extra assumptions.

Verify this page

The sharper derivation

The d'Alembert equation, H(t+u) + H(t−u) = 2H(t)H(u), is a century-old functional equation whose continuous solutions are the hyperbolic cosine and its relatives. It governs symmetric processes where the value at a sum and difference combine through the values at the parts. In Recognition Science, a framework that derives physical structure from the cost of maintaining a ledger, a discrete record of recognition events, this equation appears inside the proof that a forced cost function must take one specific form.

The classical fact, known since the eighteenth century, is that continuous solutions to this equation are exactly the hyperbolic cosine functions. The new work here is a sharper route to that conclusion. The module shows that assuming the solution is twice continuously differentiable, a mild regularity condition, is enough to reach the same answer. It does so by differentiating the equation twice, once in each variable, and then evaluating at zero. That produces a second-order ordinary differential equation, H'' = H, whose solutions are the hyperbolic sine and cosine. Adding the condition that H(0) = 1 selects the cosine.

The payoff for the framework is that one of its five founding assumptions turns out to be redundant. The original derivation of the canonical cost function J(x) = (x + 1/x)/2 − 1 required five conditions: reciprocal symmetry, zero cost at unity, a composition law, calibration, and continuity. The module proves, in a machine-checked library of formal theorems, that reciprocal symmetry is already forced by the other conditions when the solution is twice differentiable. The composition law plus normalization alone imply that the cost is reciprocal; no separate assumption is needed.

In Recognition Science, this is called the cont diff reduction, short for continuous differentiability reduction. It tightens the logical foundation: the canonical cost function follows from normalization, composition, calibration, and a mild smoothness condition. The result is a theorem in the framework's library, meaning it has been checked by a computer from first principles. The practical consequence is that the framework's central equation rests on four assumptions, not five, and the dropped one was the least physically motivated of the set.

The reduction also illustrates a general mathematical lesson: regularity assumptions can substitute for structural ones. A functional equation plus a smoothness condition can pin down a unique solution just as firmly as a longer list of axioms. For the framework, this means the cost function is not an arbitrary choice but a forced consequence of a small, natural set of requirements. The sharper derivation makes that forcing visible with less machinery.

THEOREM dAlembert_cosh_solution_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean
dAlembert_cosh_solution_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean:169 
/-- `C²` d'Alembert solutions are determined by calibration and equal `cosh`. -/
theorem dAlembert_cosh_solution_of_contDiff
    (Hf : ℝ → ℝ)
    (h_one : Hf 0 = 1)
    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
    (h_diff : ContDiff ℝ 2 Hf)
    (h_deriv2_zero : deriv (deriv Hf) 0 = 1) :
    ∀ t, Hf t = Real.cosh t := by
  have h_ode : ∀ t, deriv (deriv Hf) t = Hf t :=
    dAlembert_to_ODE_of_contDiff Hf h_dAlembert h_diff h_deriv2_zero
  have h_even : Function.Even Hf := dAlembert_even Hf h_one h_dAlembert
  have h_diff0 : DifferentiableAt ℝ Hf 0 :=
    (contDiffTwo_differentiable h_diff).differentiableAt
  have h_deriv_zero : deriv Hf 0 = 0 :=
    even_deriv_at_zero Hf h_even h_diff0
  exact ode_cosh_uniqueness_contdiff Hf h_diff h_ode h_one h_deriv_zero
THEOREM composition_law_forces_reciprocity · IndisputableMonolith/Cost/ContDiffReduction.lean
composition_law_forces_reciprocity · IndisputableMonolith/Cost/ContDiffReduction.lean:138 
/-- A normalized composition-law cost is automatically reciprocal. -/
theorem composition_law_forces_reciprocity
    (F : ℝ → ℝ)
    (hNorm : IsNormalized F)
    (hComp : SatisfiesCompositionLaw F) :
    IsReciprocalCost F := by
  intro x hx
  let Hf : ℝ → ℝ := H F
  have h_H0 : Hf 0 = 1 := by
    dsimp [Hf]
    simpa [H, G, IsNormalized] using hNorm
  have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
  have h_direct : DirectCoshAdd (G F) := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
  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
    have h_goal :
        (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 [Hf, H] using h_goal
  have h_even : Function.Even Hf := dAlembert_even Hf h_H0 h_dAlembert
  have h_even_at_log := h_even (Real.log x)
  have h_eq_plus :
      F x + 1 = F x⁻¹ + 1 := by
    simpa [Hf, H, G, Real.exp_log hx, Real.exp_neg] using h_even_at_log.symm
  linarith
THEOREM law_of_logic_forces_jcost_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean
law_of_logic_forces_jcost_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean:186 
/-- Sharpened T5 surface:
normalization, the composition law, calibration, and `C²` regularity of `H = G + 1`
already force the canonical reciprocal cost. Reciprocal symmetry is derived, not assumed. -/
theorem law_of_logic_forces_jcost_of_contDiff
    (F : ℝ → ℝ)
    (hNorm : IsNormalized F)
    (hComp : SatisfiesCompositionLaw F)
    (hCalib : IsCalibrated F)
    (h_diff : ContDiff ℝ 2 (H F)) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x := by
  intro x hx
  let Gf : ℝ → ℝ := G F
  let Hf : ℝ → ℝ := H F
  have hCoshAdd : CoshAddIdentity F := (composition_law_equiv_coshAdd F).mp hComp
  have h_direct : DirectCoshAdd Gf := CoshAddIdentity_implies_DirectCoshAdd F hCoshAdd
  have h_H0 : Hf 0 = 1 := by
    dsimp [Hf]
    simpa [H, G, IsNormalized] using hNorm
  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
    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 simp [hG]
        _ = 2 * (Gf t + 1) * (Gf u + 1) := by ring
    simpa [Hf, H, Gf] using h_goal
  have h_H_d2 : deriv (deriv Hf) 0 = 1 := by
    have hG_d2 : deriv (deriv Gf) 0 = 1 := by
      simpa [Gf, G, IsCalibrated] using hCalib
    have hderiv : deriv Hf = deriv Gf := by
      funext t
      change deriv (fun y => Gf y + 1) t = deriv Gf t
      exact deriv_add_const (f := Gf) (x := t) (c := (1 : ℝ))
    have hderiv2 : deriv (deriv Hf) = deriv (deriv Gf) := congrArg deriv hderiv
    exact (congrArg (fun g => g 0) hderiv2).trans hG_d2
  have h_H_cosh : ∀ t, Hf t = Real.cosh t :=
    dAlembert_cosh_solution_of_contDiff Hf h_H0 h_dAlembert (by simpa [Hf] using h_diff) h_H_d2
  have h_G_cosh : ∀ t, Gf t = Real.cosh t - 1 := by
    intro t
    have hH := h_H_cosh t
    have hH' : Gf t + 1 = Real.cosh t := by
      simpa [Hf, H, Gf] using hH
    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]
    _ = Gf (Real.log x) := rfl
    _ = Real.cosh (Real.log x) - 1 := h_G_cosh (Real.log x)
    _ = G Cost.Jcost (Real.log x) := by simpa using hJG.symm
    _ = Cost.Jcost (Real.exp (Real.log x)) := by simp [G]
    _ = Cost.Jcost x := by rw [ht]

What this page does not claim

The module does not prove that continuity alone is sufficient; it requires twice continuous differentiability. The reduction does not eliminate the need for calibration; that condition remains essential. The module does not address the physical meaning of the cost function, only its mathematical derivation.

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/ContDiffReduction.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