aczel_classification_conditional
plain-language theorem explainer
Continuous solutions to d'Alembert's equation that stay at or above 1 are classified as hyperbolic cosines once the auxiliary phi-multiplicativity and continuous Cauchy-to-exponential bridges are granted. Recognition Science researchers cite the result when converting the Recognition Composition Law into exponential form via the shifted cost H = J + 1. The proof first builds continuity, positivity, and multiplicativity for the auxiliary phi, invokes the exponential classification hypothesis to extract lambda, then recovers H from phi using the
Claim. Let $H : ℝ → ℝ$ be continuous with $H(0) = 1$, satisfy the d'Alembert identity $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$, obey the phi-multiplicativity condition $phi(H)(t+u) = phi(H)(t) · phi(H)(u)$ whenever $H(t), H(u) ≥ 1$, satisfy the continuous positive Cauchy-to-exponential property, and obey $H(t) ≥ 1$ for all $t$. Then there exists $λ ∈ ℝ$ such that $H(t) = cosh(λ t)$ for all real $t$.
background
In the Recognition Science setting the shifted cost is defined by $H(x) = J(x) + 1$, where $J$ satisfies the Recognition Composition Law. Under this shift the RCL becomes the d'Alembert functional equation $H(t+u) + H(t-u) = 2 H(t) H(u)$. The module introduces the auxiliary function $phi(t) = H(t) + √(H(t)² - 1)$ for the branch where $H(t) ≥ 1$ (see upstream H from CostAlgebra and the module doc on Branch 1). This auxiliary converts the d'Alembert relation into the multiplicative Cauchy equation $phi(t+u) = phi(t) · phi(t)$. The upstream theorem H_from_phi recovers the original H from phi via $H(t) = (phi(t) + phi(t)⁻¹)/2$. The hypothesis H_CauchyToExponential encodes the standard result that continuous positive multiplicative functions on the reals are exponentials.
proof idea
The proof first obtains continuity of phi(H) from continuity of H, positivity of phi(H) from the lower bound on H, and phi(H)(0) = 1 from phi_at_zero. It then applies H_PhiMultiplicative together with the lower bound to obtain multiplicativity of phi(H). Application of H_CauchyToExponential yields phi(H)(t) = exp(λ t). Finally H_from_phi combined with the identity cosh(x) = (e^x + e^{-x})/2 recovers the desired form for H.
why it matters
This theorem completes the conditional classification of d'Alembert solutions in the cosh branch, which is the one needed for the Recognition Science cost function. It directly supports the uniqueness statement for J in the forcing chain (T5) by showing that the shifted H must be a hyperbolic cosine, matching the explicit form J(x) = cosh(log x) - 1. The result remains conditional on the two bridge hypotheses H_PhiMultiplicative and H_CauchyToExponential. No downstream uses are recorded yet, leaving open the question of discharging the bridges inside the full RS development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.