representation_formula
plain-language theorem explainer
The representation formula recovers any continuous solution H to the d'Alembert equation from differences of its antiderivative Phi at shifted points. Analysts working on functional equations and regularity bootstrap would cite this identity. The proof integrates the equation over an interval, equates each integral to a Phi difference by showing the discrepancy function has vanishing derivative and vanishes at zero, then solves algebraically for H(t).
Claim. Let $Phi(H,t) := int_0^t H(s) ds$. If $H:mathbb{R}to mathbb{R}$ is continuous and obeys $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, and if $Phi(H,delta)neq 0$, then $H(t)=frac{Phi(H,t+delta)-Phi(H,t-delta)}{2 Phi(H,delta)}$ for every $t$.
background
Phi is the antiderivative operator defined by $Phi(H,t)=int_0^t H(s) ds$. The d'Alembert equation here is the additive form $H(t+u)+H(t-u)=2H(t)H(u)$. Upstream CostAlgebra supplies the shifted cost $H(x)=J(x)+1=frac12(x+x^{-1})$, under which the Recognition Composition Law becomes this equation. The module sets out the bootstrap: continuous solutions with $H(0)=1$ are shown real analytic by first obtaining an integral representation, then deriving the ODE $H''=cH$.
proof idea
Two auxiliary functions F are formed as integral minus Phi difference for the shifts $t+u$ and $t-u$. Each F is shown to have derivative zero by combining intervalIntegral.integral_hasDerivAt_right with phi_hasDerivAt and the chain rule, then is_const_of_deriv_eq_zero plus F(0)=0 forces F identically zero. The integrated d'Alembert equation then equates the sum of integrals to $2Htcdot Phi(H,delta)$, which rearranges to the claimed formula.
why it matters
The identity is invoked directly inside dAlembert_contDiff_nat to start the induction on $C^n$ regularity, the central bootstrap result of the Aczél argument. It supplies the concrete representation step referenced in the module documentation for turning continuity into differentiability. In the Recognition Science setting it underwrites the smoothness of the cost function H that appears after T5 J-uniqueness and before the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.