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. Researchers working on T5 J-uniqueness in the Recognition Science cost layer would cite it to access the smoothness classification for d'Alembert solutions. The module aggregates results from AczelTheorem, AczelProof, and FunctionalEquation without new content.

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

background

This module sits in the cost layer of Recognition Science, where the J-cost satisfies the Recognition Composition Law and the T5 uniqueness argument requires control over solutions to the associated functional equation. The imported AczelTheorem states that every continuous solution of the d'Alembert equation with $H(0)=1$ is $C^\infty$ and falls into the two families listed above. AczelProof supplies the integration-bootstrap argument that upgrades continuity to real analyticity. FunctionalEquation provides supporting lemmas for the T5 cost uniqueness proof.

proof idea

This is a module that imports AczelTheorem, AczelProof, and FunctionalEquation to expose the classification results. No new proofs are present; the structure is a re-export seam for the theorem-level payload.

why it matters in Recognition Science

The module feeds the public cost-theoretic core exposed by DimensionalConstraints.CostLayer for the dimensional constraints rebuttal. It supplies the Aczel classification that closes the smoothness step in the T5 J-uniqueness argument of the forcing chain, confirming that admissible cost functions are analytic and of hyperbolic form.

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)