Encyclopedia Cost Cost Functional Equation D Alembert To Ode General Theorem

ARTICLE 1 claim 1 theorem

Cost Functional Equation D Alembert To Ode General Theorem

A single functional equation, the d'Alembert equation, forces its smooth solutions to obey a second-order differential equation, a bridge that Recognition Science uses to prove the uniqueness of its cost function.

Verify this page

From a functional equation to a differential equation

The d'Alembert functional equation, H(t+u) + H(t-u) = 2 H(t) H(u), is a classical object in mathematics. It asks for functions H that behave like the hyperbolic cosine, cosh, in the sense that the value at a sum plus the value at a difference equals twice the product of the values. The equation appears in the study of wave propagation and in the characterization of trigonometric functions. A natural question is: what functions satisfy it? The answer depends on the regularity assumed.

If H is smooth, meaning it has derivatives of all orders, then the d'Alembert equation forces a striking consequence: the second derivative of H at any point t equals the second derivative at zero times H(t) itself. In symbols, H''(t) = H''(0) H(t). This is the theorem dAlembert_to_ODE_general_theorem in the framework's machine-checked library of formal theorems. It converts a global functional equation into a local differential equation, a bridge that makes the equation tractable. With the additional initial condition H(0) = 1, the differential equation becomes H'' = H, whose solution is cosh, up to a constant factor.

The theorem does not claim that the d'Alembert equation alone forces H to be cosh. Without the normalization H(0) = 1, the equation admits other smooth solutions, such as H(t) = cosh(kt) for any constant k. The theorem also does not claim that every continuous solution is smooth; that is a separate, deeper result. The theorem's role in Recognition Science is precise: it is a stepping stone, not the final result. The final uniqueness of the cost function J(x) = (x + 1/x)/2 - 1 requires the full set of five conditions, including the composition law and calibration, not just the d'Alembert equation.

In Recognition Science, this bridge is part of a chain that forces the cost function's form. The framework models recognition events as a ledger, a discrete record of events, and postulates that the cost of recognition obeys a composition law. The d'Alembert equation emerges after a logarithmic change of variables. The theorem dAlembert_to_ODE_general_theorem is what allows the framework to move from the functional equation to a differential equation, which is then solved uniquely. This is a key step in the proof that any cost function satisfying the five plain conditions must equal J(x). The theorem itself, however, is a general mathematical fact, independent of the framework's interpretation.

THEOREM dAlembert_to_ODE_general_theorem · IndisputableMonolith/Cost/FunctionalEquation.lean
dAlembert_to_ODE_general_theorem · IndisputableMonolith/Cost/FunctionalEquation.lean:911 
/-- **Theorem (ODE Derivation, universal coefficient)**: If H is C∞ and
satisfies d'Alembert, then `H''(t) = H''(0) * H(t)` everywhere.

This is the unnormalized form of `dAlembert_to_ODE_theorem`. -/
theorem dAlembert_to_ODE_general_theorem (H : ℝ → ℝ)
    (h_smooth : ContDiff ℝ ⊤ H)
    (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
    ∀ t, deriv (deriv H) t = deriv (deriv H) 0 * H t := by
  have hCDiff2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
  have hDiff : Differentiable ℝ H :=
    hCDiff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  have hCDiff1_H' : ContDiff ℝ 1 (deriv H) := by
    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at hCDiff2
    rw [contDiff_succ_iff_deriv] at hCDiff2
    exact hCDiff2.2.2
  have hDiffDeriv : Differentiable ℝ (deriv H) :=
    hCDiff1_H'.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  have hsh_add : ∀ (s v : ℝ), HasDerivAt (fun u => s + u) (1 : ℝ) v := fun s v => by
    have h := (hasDerivAt_id v).add_const s; simp only [id] at h
    rwa [show (fun u : ℝ => u + s) = fun u => s + u from funext fun u => add_comm u s] at h
  have hsh_sub : ∀ (s v : ℝ), HasDerivAt (fun u => s - u) (-1 : ℝ) v := fun s v => by
    have h1 : HasDerivAt (fun u : ℝ => -u) (-1 : ℝ) v := by
      have := (hasDerivAt_id v).neg; simp only [id] at this; exact this
    have h2 := h1.const_add s
    rwa [show (fun u : ℝ => s + -u) = fun u => s - u from funext fun u => by ring] at h2
  intro t
  have h_feq : (fun u => H (t + u) + H (t - u)) = (fun u => 2 * H t * H u) :=
    funext (h_dAlembert t)
  have key : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 =
             deriv (deriv (fun u => 2 * H t * H u)) 0 :=
    congr_arg (fun f => deriv (deriv f) 0) h_feq
  have lhs_eq : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 = 2 * deriv (deriv H) t := by
    have h_plus : ∀ v, HasDerivAt (fun u => H (t + u)) (deriv H (t + v)) v := fun v => by
      have hH := (hDiff (t + v)).hasDerivAt
      have hcomp := hH.comp v (hsh_add t v)
      simp only [mul_one, Function.comp_apply] at hcomp; exact hcomp
    have h_minus : ∀ v, HasDerivAt (fun u => H (t - u)) (-deriv H (t - v)) v := fun v => by
      have hH := (hDiff (t - v)).hasDerivAt
      have hcomp := hH.comp v (hsh_sub t v)
      simp only [mul_neg, mul_one, Function.comp_apply] at hcomp; exact hcomp
    have hfirst_fun : deriv (fun u => H (t + u) + H (t - u)) =
        fun v => deriv H (t + v) - deriv H (t - v) := funext fun v => by
      have heq : (fun u => H (t + u)) + (fun u => H (t - u)) =
          fun u => H (t + u) + H (t - u) := by ext u; rfl
      have h12 : deriv (fun u => H (t + u) + H (t - u)) v = deriv H (t + v) + -deriv H (t - v) := by
        rw [← heq]; exact ((h_plus v).add (h_minus v)).deriv
      linarith [show deriv H (t + v) + -deriv H (t - v) =
          deriv H (t + v) - deriv H (t - v) from by ring]
    have hd2_plus : HasDerivAt (fun v => deriv H (t + v)) (deriv (deriv H) t) 0 := by
      have hDH : HasDerivAt (deriv H) (deriv (deriv H) (t + 0)) (t + 0) :=
        (hDiffDeriv (t + 0)).hasDerivAt
      have hcomp := hDH.comp 0 (hsh_add t 0)
      simp only [mul_one, add_zero, Function.comp_apply] at hcomp; exact hcomp
    have hd2_minus : HasDerivAt (fun v => deriv H (t - v)) (-deriv (deriv H) t) 0 := by
      have hDH : HasDerivAt (deriv H) (deriv (deriv H) (t - 0)) (t - 0) :=
        (hDiffDeriv (t - 0)).hasDerivAt
      have hcomp := hDH.comp 0 (hsh_sub t 0)
      simp only [mul_neg, mul_one, sub_zero, Function.comp_apply] at hcomp; exact hcomp
    rw [congr_fun (congr_arg deriv hfirst_fun) 0]
    have heq2 : (fun v => deriv H (t + v)) - (fun v => deriv H (t - v)) =
        fun v => deriv H (t + v) - deriv H (t - v) := by ext v; rfl
    have h : deriv (fun v => deriv H (t + v) - deriv H (t - v)) 0 =
        deriv (deriv H) t - -deriv (deriv H) t := by
      rw [← heq2]; exact (hd2_plus.sub hd2_minus).deriv
    linarith [show deriv (deriv H) t - -deriv (deriv H) t = 2 * deriv (deriv H) t from by ring]
  have rhs_eq : deriv (deriv (fun u => 2 * H t * H u)) 0 =
      2 * H t * deriv (deriv H) 0 := by
    have hfirst_fun : deriv (fun u => 2 * H t * H u) = fun v => 2 * H t * deriv H v :=
      funext fun v => ((hDiff v).hasDerivAt.const_mul (2 * H t)).deriv
    have hsecond := (hDiffDeriv 0).hasDerivAt.const_mul (2 * H t)
    rw [congr_fun (congr_arg deriv hfirst_fun) 0, hsecond.deriv]
  rw [lhs_eq, rhs_eq] at key
  linarith

What this page does not claim

The d'Alembert equation alone forces H to be cosh; other smooth solutions exist without normalization. Every continuous solution of the d'Alembert equation is smooth; that is a separate theorem. This theorem proves the uniqueness of the cost function J; that requires all five conditions.

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