h_aczel_classification_proved
Continuous solutions to d'Alembert's equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 are infinitely differentiable. Researchers in functional equations and the Recognition Science cost model cite the result to eliminate the last foundational hypothesis. The proof is a one-line application of the continuity-to-C^∞ bootstrap lemma.
claimEvery continuous $H : ℝ → ℝ$ satisfying $H(0) = 1$ and $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$ is $C^∞$.
background
The module treats d'Alembert's functional equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ together with the normalization $H(0) = 1$. The predicate H_AczelClassification asserts that any such continuous real-valued H must be infinitely differentiable, with the three classical solutions 1, cosh(λt), and cos(λt) all C^∞. The local proof strategy proceeds by integration bootstrap: the equation plus the fundamental theorem of calculus yields a representation H(t) = (Φ(t+δ) − Φ(t−δ)) / (2 Φ(δ)) for an antiderivative Φ; regularity then lifts inductively from C^0 through all finite orders to C^∞, after which the ODE H'' = c H is recovered and solved by cases on the sign of c.
proof idea
The declaration is a one-line term proof that applies the lemma dAlembert_contDiff_top to the hypotheses H, h_one, h_cont, and h_dAlembert.
why it matters in Recognition Science
The theorem discharges the Aczél classification hypothesis, which had been the sole remaining foundation axiom in the IndisputableMonolith library. It thereby completes the smoothness step inside the cost functional equation module and confirms that every continuous solution belongs to one of the three families catalogued in Aczél's 1966 lectures. No open questions remain on this point; the result removes the last obstacle to unconditional use of C^∞ regularity in downstream cost arguments.
scope and limits
- Does not classify solutions that fail to be continuous.
- Does not determine the numerical value of λ from initial data.
- Does not extend the result to complex-valued or vector-valued functions.
- Does not address the equation on domains other than the reals.
formal statement (Lean)
452theorem h_aczel_classification_proved : H_AczelClassification :=
proof body
Term-mode proof.
453 fun H h_one h_cont h_dAlembert => dAlembert_contDiff_top H h_one h_cont h_dAlembert
454
455-- The typeclass-parameterized `aczel_dAlembert_smooth` lives in
456-- `IndisputableMonolith.Cost.AczelClass` and is satisfied by the
457-- `AczelSmoothnessPackage` instance in `IndisputableMonolith.Cost.AczelProof`,
458-- which delegates to `dAlembert_contDiff_top` above.
459
460end
461
462end FunctionalEquation
463end Cost
464end IndisputableMonolith