pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Cost.AczelClass

show as:
view Lean formalization →

The AczelClass module records that any continuous solution H of the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 is infinitely differentiable. Researchers on the Recognition Science T5 J-uniqueness step cite it to secure C^∞ regularity before classifying solutions. The module states the Aczél 1966 basis and defers the concrete instance to the AczelProof module.

claimAny continuous $H : ℝ → ℝ$ satisfying $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$ with $H(0)=1$ is $C^∞$.

background

Recognition Science derives the J-cost from the forcing chain T0-T8, where T5 uses the Recognition Composition Law to force J(x) = (x + x^{-1})/2 - 1. The d'Alembert equation appears after the substitution H(t) = J(e^t) + 1, converting the multiplicative relation into an additive one. This module supplies the smoothness package that lets the classification proceed from continuity alone.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the AczelProof theorem that continuous d'Alembert solutions are real analytic (ContDiff ℝ ⊤) and the FunctionalEquation helpers used in the T5 cost uniqueness proof. It supplies the smoothness step required to reach the cosh form inside the J-uniqueness argument of the forcing chain, citing Aczél 1966 Ch. 3.

scope and limits

used by (2)

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

declarations in this module (2)