representation_formula
plain-language theorem explainer
Representation formula recovers H(t) from the normalized difference of its antiderivative Phi at t shifted by ±δ. Analysts studying regularity of d'Alembert functional equations cite it to launch the bootstrap argument. Proof constructs auxiliary functions whose derivatives vanish identically, hence constants, to equate the integrals to the Phi differences.
Claim. Let $Phi(t) := ∫_0^t H(s) ds$. If $H:ℝ→ℝ$ is continuous and satisfies $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, and if $δ∈ℝ$ satisfies $Phi(δ)≠0$, then $H(t)=[Phi(t+δ)-Phi(t-δ)]/(2 Phi(δ))$ for every real $t$.
background
The module establishes that every continuous solution of the d'Alembert equation with H(0)=1 is C^∞, via integration bootstrap. Phi denotes the antiderivative ∫_0^t H(s) ds. Upstream lemmas supply that Phi has derivative H (phi_hasDerivAt) and Phi(0)=0 (phi_zero). In the CostAlgebra setting, H(x)=J(x)+1 converts the Recognition Composition Law into the stated additive d'Alembert form.
proof idea
Two auxiliary functions are defined whose derivatives are shown to vanish by combining intervalIntegral.integral_hasDerivAt_right with phi_hasDerivAt and the chain rule; each is therefore constant by is_const_of_deriv_eq_zero and evaluates to zero at the origin, yielding the shift identities for the integrals. These are added, the d'Alembert relation is substituted inside the integrand, the resulting constant multiple is integrated, and the target identity is solved by field_simp and linarith.
why it matters
The lemma supplies the representation used by dAlembert_contDiff_nat to bootstrap continuity to ContDiff n for every n, which then yields the full Aczél classification (constant, cosh, or cos). It removes the last external hypothesis in the IndisputableMonolith cost algebra. In the Recognition Science chain it converts the algebraic form of the Recognition Composition Law into the analytic regularity required for the phi-ladder and mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.