module module high

`IndisputableMonolith.Cost.AczelTheorem`

The module proves that every solution to the d'Alembert functional equation is even. Researchers classifying solutions for the T5 cost uniqueness proof cite it as an early step in the Aczel chain. The argument is a direct substitution using properties imported from the FunctionalEquation module.

claimIf $H : ℝ → ℝ$ satisfies $H(t + u) + H(t - u) = 2 H(t) H(u)$ with $H(0) = 1$, then $H(-t) = H(t)$ for all $t$.

background

The module belongs to the Cost domain and imports lemmas from FunctionalEquation, described as supplying helpers for the T5 cost uniqueness proof. It states H1 as the evenness property of d'Alembert solutions. The local setting is the functional equation whose continuous solutions are later classified into cosh-type or cosine-type branches in downstream packages.

proof idea

The module contains the direct argument for evenness via substitution of $u = -t$ into the imported functional equation. This is a one-line wrapper that applies the core equation properties.

why it matters in Recognition Science

This module feeds AczelClassification and AczelProof, which use evenness to reach smoothness and the calibrated ODE $H'' = H$. It supplies the first step in the Aczel classification package that closes the T5 forcing chain toward J-uniqueness.

scope and limits

Does not assume or prove continuity of solutions.
Does not derive the explicit form of H.
Does not address differentiability or analyticity.

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