cosh_satisfies_dAlembert
plain-language theorem explainer
The declaration shows that the hyperbolic cosine satisfies the d'Alembert functional equation H(t + u) + H(t - u) = 2 H(t) H(u) with H(0) = 1. Analysts of the Recognition Science forcing chain cite this to verify the canonical form of the shifted log-lift in the Fourth Gate. The proof is a direct term-mode verification that applies the addition and subtraction identities for cosh followed by linear arithmetic.
Claim. $H(0) = 1$ and $H(t + u) + H(t - u) = 2 H(t) H(u)$ for all real $t, u$, where $H(t) = {cosh}(t)$.
background
The Fourth Gate module formalizes the d'Alembert structure condition as a derived cross-check. In the Option A formulation, Gate 3 assumes the normalized ODE G''(t) = G(t) + 1 together with evenness and calibration, which forces G(t) = cosh(t) - 1; the shifted log-lift H = G + 1 therefore satisfies the functional equation automatically. The module records the classical result that continuous solutions to f(x + y) + f(x - y) = 2 f(x) f(y) are exactly cosh(λx) for λ real.
proof idea
The term proof applies constructor to split the conjunction in SatisfiesDAlembert. The zero condition is closed by exact Real.cosh_zero. The functional equation is handled by introducing t and u, obtaining the addition and subtraction identities via Real.cosh_add and Real.cosh_sub, then discharging with linarith.
why it matters
This instance feeds the parent theorem Jcost_has_dAlembert_structure, which lifts the result to the cost function Jcost. It completes the explicit certificate path for the Fourth Gate, confirming that the hyperbolic branch arising from the curvature gate also satisfies the classical d'Alembert equation studied by d'Alembert. In the forcing chain it anchors the J-uniqueness step (T5) by exhibiting the explicit solution that later forces the phi fixed point and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.