aczel_classification_conditional
plain-language theorem explainer
Researchers classifying continuous solutions to the d'Alembert equation with H(0)=1 and H >=1 everywhere would cite this result to conclude H equals cosh(lambda t). It assumes the functional equation, continuity, and the two bridge properties that convert the auxiliary phi into an exponential. The proof constructs phi, verifies the continuous multiplicative Cauchy equation on phi, invokes the exponential form, and recovers H algebraically.
Claim. Let $H:\mathbb{R}\to\mathbb{R}$ be continuous, satisfy $H(0)=1$, obey the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, obey $H(t)\ge1$ for all $t$, and satisfy the auxiliary multiplicative property $\phi(t+u)=\phi(t)\phi(t)$ together with the continuous positive Cauchy-to-exponential bridge, where $\phi(t)=H(t)+\sqrt{H(t)^2-1}$. Then there exists $\lambda\in\mathbb{R}$ such that $H(t)=\cosh(\lambda t)$ for all $t$.
background
The module develops the cosh branch of the Aczél classification for continuous solutions of d'Alembert's equation that stay at or above 1. The auxiliary function is defined by $\phi(t)=H(t)+\sqrt{H(t)^2-1}$; the referenced def H_PhiMultiplicative states that d'Alembert plus $H\ge1$ forces $\phi(t+u)=\phi(t)\phi(u)$. The referenced def H_CauchyToExponential encodes the standard result that a continuous positive multiplicative function with value 1 at 0 must be an exponential.
Upstream, the CostAlgebra def H reparametrizes the Recognition Composition Law as the d'Alembert equation: H(x)=J(x)+1 where J is the shifted cost. The local setting (MODULE_DOC) isolates the cosh case because J-cost grows unboundedly, so H exceeds 1. The upstream theorem H_from_phi recovers H from phi via the identity H(t)=(phi(t)+phi(t)^{-1})/2. The upstream theorem phi_at_zero gives phi(0)=1 when H(0)=1.
proof idea
The tactic proof first shows phi H is continuous by unfolding the definition and using continuity of H together with square-root and arithmetic operations. It records positivity of phi from the referenced phi_pos, the value 1 at zero from phi_at_zero, and multiplicativity from H_PhiMultiplicative applied to the given H_ge_one. It then applies the hypothesis H_CauchyToExponential to obtain lambda such that phi(t)=exp(lambda t). Finally it invokes H_from_phi, substitutes the exponential, and converts to cosh using the identity Real.cosh_eq together with exp_neg.
why it matters
This theorem supplies the full Aczél classification for the cosh branch, conditional on the two bridge lemmas H_PhiMultiplicative and H_CauchyToExponential. It directly supports the Recognition Science cost analysis by classifying solutions to the reparametrized RCL that arise from J-uniqueness (T5). The result sits inside the forcing chain that produces the eight-tick octave and D=3; it is the step that converts the functional equation into the explicit hyperbolic form used for mass ladders and the alpha band. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.