dAlembert_to_ODE_general_theorem
plain-language theorem explainer
A smooth function H obeying the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) for all real t,u satisfies the ODE H''(t) = H''(0) H(t). Recognition Science workers cite this when converting the T5 cost uniqueness problem into an ODE whose solutions are multiples of cosh. The argument first extracts twice differentiability from the C^∞ hypothesis, equates the second derivatives at zero of both sides of the functional equation after fixing t, and matches the resulting coefficients via direct computation of the chain-rule derivatives.
Claim. Let $H:\mathbb{R}\to\mathbb{R}$ be infinitely differentiable. If $H(t+u)+H(t-u)=2H(t)H(u)$ holds for all real $t,u$, then the second derivative satisfies $H''(t)=H''(0)\cdot H(t)$ for every real $t$.
background
The module supplies functional-equation lemmas that support the T5 J-uniqueness argument. Here H is the shifted cost reparametrization H_F(t)=G_F(t)+1; the sibling definition in CostAlgebra states that the shifted cost H(x)=J(x)+1 equals ½(x+x^{-1}) and converts the Recognition Composition Law into the displayed d'Alembert equation.
Upstream CostAlgebra.H records that this H satisfies H(xy)+H(x/y)=2H(x)H(y). The present theorem supplies the un-normalized ODE bridge; its normalized sibling assumes the extra datum H''(0)=1.
proof idea
The tactic proof first obtains ContDiff ℝ 2 H and Differentiable ℝ (deriv H) from the C^∞ hypothesis. It fixes t, equates the two sides of the functional equation, and shows that their second derivatives at zero coincide. The left-hand side is differentiated twice using HasDerivAt on the shifts t+u and t-u together with the chain rule; this produces the factor 2 deriv(deriv H) t. The right-hand side is differentiated twice by the product rule and yields 2 H(t) deriv(deriv H) 0. Equating the two expressions and rearranging finishes the argument.
why it matters
The result supplies the general ODE bridge invoked by dAlembert_to_ODE_general and aczel_kannappan_via_cases inside AxiomDischargePlan. Those theorems assemble the case analysis that discharges the Aczél–Kannappan axiom for the T5 uniqueness step. The derivation therefore links the Recognition Composition Law directly to the differential equation whose solutions are scalar multiples of cosh, the form required by J-uniqueness at T5.
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β(τ,ℓ)"