pith. sign in
module module high

IndisputableMonolith.Cost.CauchyAuxiliary

show as:
view Lean formalization →

The CauchyAuxiliary module supplies auxiliary definitions that convert d'Alembert solutions H into exponential form via the map phi. Researchers classifying continuous solutions to the functional equation or deriving exponential representations in the cost framework cite it. The module consists of definitions and one conditional classification that rests directly on the imported Aczel theorem.

claimFor continuous solutions $H$ of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ and $H(t)geq 1$, define the auxiliary map $phi(t)=H(t)+sqrt(H(t)^2-1)$.

background

The module sits inside the Cost domain and imports the Aczel theorem, which states that every continuous solution of $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is $C^infty$ and equals either the constant 1 or $cosh(lambda t)$ for some lambda. It introduces the auxiliary function phi together with supporting definitions (phi at zero, positivity, H recovered from phi, and the multiplicative property of H). These objects prepare the conversion of hyperbolic solutions into exponential form while remaining inside the Recognition Science treatment of Cauchy-type equations.

proof idea

This is a definition module, no proofs. It declares the map phi and its immediate companions, then records a conditional classification statement that applies the Aczel smoothness result.

why it matters in Recognition Science

The module bridges the Aczel classification to the exponential and phi-ladder constructions used in cost analysis. It supplies the conversion tool required by downstream results on H_PhiMultiplicative and the conditional aczel classification. The parent result is the Aczel theorem on smoothness of d'Alembert solutions.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)