pith. sign in
module module high

IndisputableMonolith.Cost.AczelClassification

show as:
view Lean formalization →

The AczelClassification module extracts the theorem-level payload from the Aczel classification seam for use in cost-theoretic arguments. Researchers verifying T5 uniqueness in the Recognition Science forcing chain would cite it to access smoothness of d'Alembert solutions. The module assembles the fully proved Aczel smoothness theorem from its dedicated proof and theorem components without additional derivation.

claimEvery continuous solution $H:\mathbb{R}\to\mathbb{R}$ of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is $C^\infty$, with the solutions $H(t)=1$ or $H(t)=\cosh(\lambda t)$ for some $\lambda$.

background

This module sits inside the cost layer of Recognition Science and imports three upstream modules. AczelProof establishes that any continuous solution of the d'Alembert equation is real analytic via an integration bootstrap that upgrades continuity to $C^\infty$. AczelTheorem states the complete classification: the only continuous solutions with $H(0)=1$ are the constant 1 and the hyperbolic cosines. FunctionalEquation supplies supporting lemmas for the T5 cost uniqueness argument that employs the Recognition Composition Law.

proof idea

This is a definition module, no proofs. It packages the statements and analyticity result already established in the imported AczelTheorem and AczelProof modules for clean re-export.

why it matters in Recognition Science

The module supplies the Aczel classification to the CostLayer inside DimensionalConstraints, which packages the public cost-theoretic core used in the dimensional constraints rebuttal. It closes the seam needed for T5 J-uniqueness by guaranteeing that continuous solutions of the governing functional equation are analytic, thereby licensing the identification of J with the cosh form that appears in the phi-ladder and the eight-tick octave.

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)