Cost Cont Diff Reduction D Alembert To Ode Of Cont Diff

The regularity bridge

The d'Alembert equation, H(t+u) + H(t-u) = 2H(t)H(u), is a classical functional equation whose continuous solutions are the hyperbolic cosine and the ordinary cosine. The theorem d'Alembert_to_ODE_of_contDiff in the machine-checked library of formal theorems shows that if a solution is twice continuously differentiable and its second derivative at zero equals 1, then it satisfies the ordinary differential equation H''(t) = H(t). This is the bridge from a functional equation, which constrains values across the whole line at once, to a local differential equation that can be solved by standard methods.

The proof is a short chain of differentiations. Differentiating the d'Alembert equation once with respect to the second variable yields an identity relating first derivatives. Setting the second variable to zero and differentiating again gives 2H''(t) = 2H(t)H''(0). The calibration condition H''(0) = 1 then reduces this to H''(t) = H(t). The argument requires the twice-differentiability hypothesis at each step, which is exactly what the ContDiff condition supplies: a function whose first two derivatives exist and are continuous.

The same regularity hypothesis also forces the solution to be exactly the hyperbolic cosine. A companion theorem in the same module shows that a twice continuously differentiable d'Alembert solution with H(0) = 1 and H''(0) = 1 must equal cosh(t) everywhere. This is the classical uniqueness result for the d'Alembert equation under smoothness, and it is what makes the later identification of the cost function possible.

In Recognition Science, this theorem removes a portion of the regularity seam in the derivation of the canonical cost function. The framework's composition law, together with normalization and calibration, already forces reciprocal symmetry; the ContDiff reduction shows that on the smooth surface, the full cost function follows from normalization, composition, and calibration alone. The theorem does not claim that the d'Alembert equation has only smooth solutions. Without the twice-differentiability hypothesis, there are wild solutions built using Hamel bases, and the theorem says nothing about them. It also does not derive the cost function from the d'Alembert equation by itself; the calibration condition H''(0) = 1 is an additional input, not a consequence of the equation.

/-- A `C²` d'Alembert solution with calibrated second derivative satisfies `H'' = H`. -/
theorem dAlembert_to_ODE_of_contDiff
    (Hf : ℝ → ℝ)
    (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, deriv (deriv Hf) t = Hf t := by
  intro t
  have h_rel := dAlembert_second_deriv_at_zero_of_contDiff Hf h_dAlembert h_diff t
  rw [h_deriv2_zero] at h_rel
  linarith

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

/-- 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 theorem does not apply to non-smooth solutions of the d'Alembert equation. The theorem does not derive the calibration condition H''(0) = 1 from the equation itself. The theorem does not by itself establish the full cost function; it is one step in a longer chain.

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: