dAlembert_to_ODE_general_theorem
plain-language theorem explainer
Smooth functions H satisfying the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) obey the linear ODE H''(t) = H''(0) H(t) for all t. Recognition Science cost theorists cite this when reducing the Recognition Composition Law to a differential equation inside the T5 J-uniqueness argument. The proof fixes t, equates second derivatives at zero of the two sides of the functional equation, and evaluates the left side via the chain rule on shifted arguments to obtain twice the second derivative at t.
Claim. If $H : ℝ → ℝ$ is $C^∞$ and satisfies $H(t + u) + H(t - u) = 2 H(t) H(u)$ for all real $t, u$, then $H''(t) = H''(0) · H(t)$ for all $t ∈ ℝ$.
background
In the Cost.FunctionalEquation module, which supplies helpers for the T5 J-uniqueness argument, H is the shifted cost H_F(t) := G_F(t) + 1. This reparametrization converts the Recognition Composition Law into the classical d'Alembert equation. Upstream, the CostAlgebra module defines the unshifted H(x) = J(x) + 1 = (x + x^{-1})/2, whose multiplicative property yields exactly this additive form after the change of variables x = e^t.
proof idea
The proof first extracts C² differentiability from the C^∞ hypothesis. It fixes arbitrary t and equates the second derivatives at zero of f(u) = H(t+u) + H(t-u) and g(u) = 2 H(t) H(u). Direct computation of the second derivative of f at 0, using HasDerivAt on the shifted arguments together with the chain rule and additivity, yields 2 H''(t). The corresponding computation for g yields 2 H(t) H''(0). Equating and rearranging produces the ODE.
why it matters
This result is invoked by the AxiomDischargePlan module inside aczel_kannappan_via_cases and the wrapper dAlembert_to_ODE_general. It supplies the universal-coefficient form needed for the T5 forcing chain, where J-uniqueness follows once solutions to the cost equation are shown to satisfy the ODE whose solutions are classified by the eight-tick octave. The calculation closes the reduction from the Recognition Composition Law to the differential equation without requiring normalization of H''(0).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 10 of 10)
-
Quantum gravity breaks acceleration-thermal equivalence for atoms
"the appearance of terms ... proportional to a^4 and a^2 indicates that the equivalence ... is lost ... derivatives of the Wightman function increase the order of the pole in the sinh function ... higher the order of the pole, the higher the powers of a"
-
Convex factors let energy models scale to larger reasoning tasks
"Because convexity is preserved under summation, the global relaxed objective remains convex... first-order optimality condition at the target solution is enough to certify global optimality"
-
Finsler spacetimes split diffeomorphically under timelike completeness
"the p-d’Alembertian... is elliptic... yielding a simpler, alternative proof of the timelike splitting theorem"
-
Free energy minimization yields convergent policy composition
"GateFrame casts gating as minimization of statistical complexity (KL) minus ε-entropy subject to mixture-of-primitives constraint; this is shown equivalent to expected free energy when q ∝ q̃ exp(−c)."
-
Exact flow replaces Euler step in delta-rule attention
"St = e^{-βt At} St-1 + ∫ e^{-(βt-τ)At} bt dτ ... e^{-βt At} = I - (1-e^{-βt λt})/λt At ... St = (I - αt kt k^T) St-1 + αt kt v^T"
-
Quadratic cost correction lifts VLA success 28.8% in dynamic scenes
"The companion matrix has eigenvalues φ±2 where φ=(1+√5)/2 is the golden ratio. ... δ_k^* = (1 - F_{2k+1}/F_{2K+1}) v d̂_⊥ ... Lucas-polynomial second-order branch Λ_k(K)"
-
Hyperbolic field encodes 3D scene hierarchies from 2D cues
"We use the D-dimensional Lorentz model H^D_c ... projection ... angular classification ... LCA ordering loss ... do(i,j) hyperbolic distance surrogate"
-
Intervention complexity defines canonical rewards for intelligence
"ρ-intervention complexity is the minimum ρ-cost of a program achieving a given state transition... five natural properties... minimality: ICρμ depends on Iμ(s,s′) only through the minimum, discarding all suboptimal interventions."
-
Symmetric generators tighten equivalence-query round bounds
"Definition 1 (Symmetric counterexample generators) ... CE(h, c|...) = CE(c, h|...) ... Payoff(h, c) + Payoff(c, h) ≤ 1 ... minimax theorem implies ... Payoff(p, q) ≤ 1/2 ... version space shrinks by a factor of at least 2 ... Ldim drops by at least one with constant probability"
-
Chaos model captures dissipation across space and time
"the GMC appears as an appropriate statistically homogeneous model of the turbulent dissipation field... propose a generalization to a spatio-temporal framework... Clnε(ℓ) = μ ln+(L/|ℓ|) + μ fNS(ℓ) ... CXβ(τ,ℓ) = ln+ (L / max(2π|ℓ|,(D3 τ)^{1/2β})) + fXβ(τ,ℓ)"