Pith. sign in
module module high

IndisputableMonolith.Cost.AczelTheorem

show as:
view Lean formalization →

The AczelTheorem module proves every d'Alembert solution is even (H1). Researchers on the T5 J-uniqueness step cite it to advance the d'Alembert forcing chain. Proofs apply functional-equation substitutions imported from the core FunctionalEquation module to derive evenness plus local boundedness and double-angle relations.

claimIf $H:\mathbb{R}\to\mathbb{R}$ satisfies $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$ with $H(0)=1$, then $H(t)=H(-t)$ for all $t$.

background

This module lies in the Cost domain and supplies auxiliary results for the T5 cost uniqueness proof. It imports from IndisputableMonolith.Cost.FunctionalEquation, whose doc states it provides lemmas for the T5 cost uniqueness proof. The d'Alembert equation is the relation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$, as quoted in the downstream AczelProof module.

proof idea

The module collects lemmas around the d'Alembert equation. Core result dAlembert_even' follows by direct substitution of specific arguments into the functional equation. Companion lemmas establish local boundedness and the double-angle formula as intermediate steps.

why it matters in Recognition Science

The module supplies H1 (evenness of d'Alembert solutions) that feeds AczelClassification, which packages the d'Alembert forcing chain, and AczelProof, which establishes real analyticity of continuous solutions. It advances the T5 step in the Recognition Science framework by enabling the smoothness branch of the Aczel classification strategy.

scope and limits

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (20)