Encyclopedia Cost Cost Cont Diff Reduction D Alembert Cosh Solution Of Cont Diff

ARTICLE 3 claims 3 theorems

Cost Cont Diff Reduction D Alembert Cosh Solution Of Cont Diff

A smooth function obeying a classical symmetry equation must be the hyperbolic cosine, a fact that pins down the framework's cost of recognition.

Verify this page

The smooth solution

The classical d'Alembert equation, written for a function H of a real variable, is H(t+u) + H(t−u) = 2 H(t) H(u). Its smooth solutions are exactly the hyperbolic cosine, cosh, and the ordinary cosine, cos, along with their constant multiples. The equation expresses a kind of self-similarity: the value at a sum and difference is determined by the product of the values at the parts. This functional equation has a long history, appearing in work on the wave equation and on trigonometric addition formulas.

In the Recognition Science framework, the function H is a shifted version of the cost, a number that measures the price of recognizing one event as another. The framework's central object is a ledger, a discrete record of such recognition events. The cost is forced, not chosen: any function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 − 1. The declaration dAlembert_cosh_solution_of_contDiff is a lemma in the framework's machine-checked library of formal theorems. It states that if H is twice continuously differentiable, satisfies the d'Alembert equation, has H(0) = 1, and has second derivative at zero equal to 1, then H(t) = cosh(t) for all t.

The proof works by differentiating the d'Alembert equation. First, differentiate once in the second variable to get a relation between first derivatives. Then set u = 0 and differentiate again to obtain an equation linking the second derivative of H at t to the second derivative at 0. The calibration condition, that the second derivative at 0 equals 1, turns this into the ordinary differential equation H'' = H. With the initial conditions H(0) = 1 and H'(0) = 0 (which follows from the d'Alembert equation), the unique solution is cosh.

This result matters because it removes an assumption. Earlier work in the framework assumed reciprocal symmetry, the condition that the cost of recognizing x as y equals the cost of recognizing y as x. The declaration composition_law_forces_reciprocity shows that this symmetry follows from the composition law and normalization alone. The cosh solution then shows that, on the smooth surface, the canonical reciprocal cost follows from just three conditions: normalization, composition, and calibration. The framework proves that the cost function is unique, and this lemma is a step in that proof.

The declaration does not claim that every solution of the d'Alembert equation is cosh. Without the smoothness condition, there are pathological solutions, such as those built from Hamel bases of the real numbers as a vector space over the rationals. It also does not claim that the framework derives the value of any physical constant, such as the fine-structure constant. The result is a theorem about a functional equation, not a statement about the physical world.

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 dAlembert_first_deriv_of_contDiff · dAlembert_second_deriv_at_zero_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean
dAlembert_first_deriv_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean:43 
/-- Differentiate the d'Alembert equation once in the second variable. -/
theorem dAlembert_first_deriv_of_contDiff
    (Hf : ℝ → ℝ)
    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
    (h_diff : ContDiff ℝ 2 Hf) :
    ∀ t u, deriv Hf (t + u) - deriv Hf (t - u) = 2 * Hf t * deriv Hf u := by
  intro t u
  have h_diff1 : Differentiable ℝ Hf := contDiffTwo_differentiable h_diff
  have h_plus :
      HasDerivAt (fun v => Hf (t + v)) (deriv Hf (t + u)) u := by
    have h_inner : HasDerivAt (fun v => t + v) 1 u := by
      simpa using (hasDerivAt_const u t).add (hasDerivAt_id u)
    simpa using (h_diff1.differentiableAt (x := t + u)).hasDerivAt.comp u h_inner
  have h_minus :
      HasDerivAt (fun v => Hf (t - v)) (-deriv Hf (t - u)) u := by
    have h_inner : HasDerivAt (fun v => t - v) (-1) u := by
      simpa using (hasDerivAt_const u t).sub (hasDerivAt_id u)
    simpa using (h_diff1.differentiableAt (x := t - u)).hasDerivAt.comp u h_inner
  have h_left :
      HasDerivAt (fun v => Hf (t + v) + Hf (t - v))
        (deriv Hf (t + u) - deriv Hf (t - u)) u := by
    simpa using h_plus.add h_minus
  have h_const : HasDerivAt (fun _ : ℝ => 2 * Hf t) 0 u :=
    hasDerivAt_const u (2 * Hf t)
  have h_right :
      HasDerivAt (((fun _ : ℝ => 2 * Hf t) * Hf)) (2 * (Hf t * deriv Hf u)) u := by
    simpa [mul_assoc] using h_const.mul ((h_diff1.differentiableAt (x := u)).hasDerivAt)
  have h_eq :
      (fun v => Hf (t + v) + Hf (t - v)) = ((fun _ : ℝ => 2 * Hf t) * Hf) := by
    funext v
    simpa [Pi.mul_apply, mul_assoc] using h_dAlembert t v
  have h_deriv_eq := congrArg (fun f : ℝ → ℝ => deriv f u) h_eq
  change deriv (fun v => Hf (t + v) + Hf (t - v)) u =
      deriv (((fun _ : ℝ => 2 * Hf t) * Hf)) u at h_deriv_eq
  rw [h_left.deriv, h_right.deriv] at h_deriv_eq
  simpa [mul_assoc] using h_deriv_eq
dAlembert_second_deriv_at_zero_of_contDiff · IndisputableMonolith/Cost/ContDiffReduction.lean:80 
/-- Differentiate the first-derivative identity at `u = 0` to relate `H''(t)` to `H''(0)`. -/
theorem dAlembert_second_deriv_at_zero_of_contDiff
    (Hf : ℝ → ℝ)
    (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
    (h_diff : ContDiff ℝ 2 Hf) :
    ∀ t, 2 * deriv (deriv Hf) t = 2 * Hf t * deriv (deriv Hf) 0 := by
  intro t
  have h_first :
      (fun u => deriv Hf (t + u) - deriv Hf (t - u)) =
        ((fun _ : ℝ => 2 * Hf t) * deriv Hf) := by
    funext u
    simpa [Pi.mul_apply, mul_assoc] using
      dAlembert_first_deriv_of_contDiff Hf h_dAlembert h_diff t u
  have h_plus :
      HasDerivAt (fun u => deriv Hf (t + u)) (deriv (deriv Hf) t) 0 := by
    have h_inner : HasDerivAt (fun u => t + u) 1 0 := by
      simpa using (hasDerivAt_const 0 t).add (hasDerivAt_id 0)
    simpa using (hasDerivAt_deriv_of_contDiffTwo h_diff (t + 0)).comp 0 h_inner
  have h_minus_raw :
      HasDerivAt (fun u => deriv Hf (t - u)) (-deriv (deriv Hf) t) 0 := by
    have h_inner : HasDerivAt (fun u => t - u) (-1) 0 := by
      simpa using (hasDerivAt_const 0 t).sub (hasDerivAt_id 0)
    simpa using (hasDerivAt_deriv_of_contDiffTwo h_diff (t - 0)).comp 0 h_inner
  have h_left_raw :
      HasDerivAt (fun u => deriv Hf (t + u) - deriv Hf (t - u))
        (deriv (deriv Hf) t + deriv (deriv Hf) t) 0 := by
    simpa using h_plus.sub h_minus_raw
  have h_const : HasDerivAt (fun _ : ℝ => 2 * Hf t) 0 0 :=
    hasDerivAt_const 0 (2 * Hf t)
  have h_right :
      HasDerivAt (((fun _ : ℝ => 2 * Hf t) * deriv Hf))
        (2 * (Hf t * deriv (deriv Hf) 0)) 0 := by
    simpa [mul_assoc] using h_const.mul (hasDerivAt_deriv_of_contDiffTwo h_diff 0)
  have h_deriv_eq := congrArg (fun f : ℝ → ℝ => deriv f 0) h_first
  change deriv (fun u => deriv Hf (t + u) - deriv Hf (t - u)) 0 =
      deriv (((fun _ : ℝ => 2 * Hf t) * deriv Hf)) 0 at h_deriv_eq
  rw [h_left_raw.deriv, h_right.deriv] at h_deriv_eq
  linarith
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

What this page does not claim

The declaration does not claim that every solution of the d'Alembert equation is cosh. The declaration does not claim that the framework derives the fine-structure constant. The declaration does not claim that the cost function is unique without the smoothness condition.

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