module module high

`IndisputableMonolith.Cost.AczelTheorem`

The module establishes that every d'Alembert solution satisfies evenness. Researchers tracing the T5 cost uniqueness step in Recognition Science cite it as the H1 symmetry lemma before smoothness arguments. The argument imports the functional equation from the upstream module and applies direct substitutions to obtain H(-t) = H(t). Sibling definitions such as dAlembert_even' organize the local steps.

claimEvery solution $H : ℝ → ℝ$ of the d'Alembert equation $H(t + u) + H(t - u) = 2 H(t) H(u)$ with $H(0) = 1$ satisfies $H(-t) = H(t)$.

background

The module belongs to the Cost domain and imports FunctionalEquation, whose doc-comment states it supplies lemmas for the T5 cost uniqueness proof. The d'Alembert equation appears here as the governing relation for J-cost and defectDist within the Recognition framework. Upstream results supply the base functional equation without continuity assumptions, while the module adds the evenness property H1 as the first classification step.

proof idea

The module organizes its content around the evenness claim H1. It defines auxiliary siblings including dAlembert_even', dAlembert_locally_bounded and dAlembert_double_angle, then applies substitutions drawn from the imported functional equation. The structure prepares the ground for the two-branch classification that appears in downstream modules.

why it matters in Recognition Science

This module supplies the H1 evenness fact that AczelClassification and AczelProof consume to reach smoothness and the ODE kernel H'' = H. It occupies the symmetry slot in the d'Alembert forcing chain that supports T5 J-uniqueness. Downstream doc-comments describe it as packaging the Aczel-supplied portion of the classification before the unconditional core is reached.

scope and limits

Does not assume continuity or measurability of H.
Does not derive smoothness or analyticity.
Does not classify solutions into cosh or cosine branches.
Does not reach the full T5 uniqueness statement.
Does not address the phi-ladder or mass formulas.

used by (5)

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

IndisputableMonolith.Cost.AczelClassification module_import
IndisputableMonolith.Cost.AczelProof module_import
IndisputableMonolith.Cost.CauchyAuxiliary module_import
IndisputableMonolith.Cost.FunctionalEquationAczel module_import
IndisputableMonolith.Foundation.PolynomialityFromLogic module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.FunctionalEquation module_import

declarations in this module (20)

theorem dAlembert_even' L44
theorem dAlembert_locally_bounded L56
theorem dAlembert_double_angle L67
def H_AczelClassification L82
abbrev smooth L93
def Phi L95
lemma phi_zero L97
lemma phi_hasDerivAt L100
lemma phi_differentiable L105
lemma deriv_phi_eq L109
lemma exists_integral_ne_zero L112
lemma representation_formula L130
lemma phi_contDiff_succ L197
theorem dAlembert_contDiff_nat L206
theorem dAlembert_contDiff_smooth L224
theorem dAlembert_to_ODE_general L231
theorem ode_neg_zero_uniqueness L288
theorem ode_cos_uniqueness L315
theorem dAlembert_contDiff_top L353
theorem h_aczel_classification_proved L452