dAlembert_cosh_solution_aczel
plain-language theorem explainer
Any continuous real-valued function H satisfying H(0) equals 1, the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) for all real t and u, and second derivative 1 at the origin must equal the hyperbolic cosine. Researchers closing uniqueness statements for the J-cost function under the Recognition Composition Law cite this result to obtain the explicit cosh form while avoiding separate regularity parameters. The argument extracts infinite differentiability from the Aczél smoothness package, derives the ODE H'' equals H, and applies the ODE-unw
Claim. Let $H : ℝ → ℝ$ be continuous with $H(0) = 1$, satisfying $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$, and with second derivative of $H$ at 0 equal to 1. Then $H(t) = cosh(t)$ for all real $t$.
background
In CostAlgebra the shifted cost is defined by $H(x) = J(x) + 1$, where $J$ satisfies the Recognition Composition Law. Under this change of variable the RCL becomes exactly the d'Alembert equation appearing in the hypotheses. The present module isolates Aczél-dependent closure theorems that assume an external smoothness package rather than the axiom-free core of FunctionalEquation.
proof idea
Term-mode construction. aczel_dAlembert_smooth yields ContDiff ℝ ⊤ H. Differentiability and evenness follow from dAlembert_even and even_deriv_at_zero. dAlembert_to_ODE_theorem supplies the ODE deriv(deriv H) t = H t. The final step applies ode_cosh_uniqueness_contdiff to the C² function under the ODE and the initial conditions H(0)=1, H'(0)=0.
why it matters
Supplies the cosh identification required by washburn_uniqueness_aczel, which asserts uniqueness of the J-cost among reciprocal costs obeying the RCL, normalization, calibration and continuity. It participates in the Aczél-based discharge path and feeds the unconditional d'Alembert results in Foundation.DAlembert.FullUnconditional. Within Recognition Science it closes the passage from the d'Alembert equation (RCL under the H substitution) to the explicit form matching the T5 J-uniqueness landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.