pith. sign in
module module high

IndisputableMonolith.Cost.AczelClassification

show as:
view Lean formalization →

This module extracts the theorem-level payload from the Aczel classification seam, packaging the smoothness results for continuous solutions of the d'Alembert functional equation. Researchers working on the T5 J-uniqueness step in Recognition Science cite it to obtain the analyticity of H that feeds cost classification. The module aggregates the complete classification (constant 1 or cosh forms) from its three imports without adding new proofs.

claimEvery continuous solution $H:ℝ→ℝ$ of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is $C^∞$ and equals either the constant function 1 or $H(t)=cosh(λt)$ for some constant $λ$.

background

The module sits inside the Cost domain and imports three files that together supply the Aczel classification for T5 cost uniqueness. AczelTheorem states that every continuous solution of the d'Alembert equation is $C^∞$, with the explicit forms 1 and cosh(λt). AczelProof supplies the integration-bootstrap argument that upgrades continuity to real analyticity. FunctionalEquation supplies supporting lemmas for the T5 cost-uniqueness proof that invokes this classification.

proof idea

This is a definition module, no proofs. It imports AczelTheorem, AczelProof, and FunctionalEquation and re-exports their statements under a single namespace for downstream use in the cost layer.

why it matters in Recognition Science

The module feeds IndisputableMonolith.Foundation.DimensionalConstraints.CostLayer, which packages the public cost-theoretic core for the dimensional constraints rebuttal. It supplies the Aczel smoothness result required by the T5 J-uniqueness argument in the forcing chain.

scope and limits

used by (1)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (10)