dAlembert_forces_Gcosh
plain-language theorem explainer
Under the d'Alembert functional equation on the shifted lift H = G + 1 together with C² smoothness, even symmetry, G(0) = 0 and unit second derivative at the origin, G must equal cosh minus one. Recognition Science invokes this to certify that the fourth gate is satisfied once curvature and calibration are fixed. The argument constructs H, verifies its derivative conditions from evenness, applies the unit-calibration lemma to H, and subtracts the constant.
Claim. Let $G : ℝ → ℝ$ be twice continuously differentiable and even with $G(0) = 0$ and $G''(0) = 1$. If the shifted function $H(t) := G(t) + 1$ satisfies $H(0) = 1$ and $H(t + u) + H(t - u) = 2 H(t) H(u)$ for all real $t, u$, then $G(t) = cosh t - 1$ for all $t ∈ ℝ$.
background
The Fourth Gate module encodes the classical d'Alembert functional equation as a structural constraint on the shifted log-lift. A function H satisfies SatisfiesDAlembert when H(0) = 1 and H(t+u) + H(t-u) = 2 H(t) H(u) for all t, u. In the Recognition Science setting this equation arises directly from the Recognition Composition Law once the cost function is reparametrized to log-coordinates via G_F(t) = F(exp t) and H = G + 1.
proof idea
The proof defines H as G plus one and confirms that H inherits C² smoothness from G. Evenness of G implies H'(0) = 0 because the derivative of an even function vanishes at zero. The second-derivative calibration passes directly to H. The argument then applies the lemma dAlembert_with_unit_calibration to obtain H(t) = cosh t, from which G(t) = cosh t - 1 follows by subtraction.
why it matters
This result closes the explicit identification step inside the Fourth Gate and is invoked by the downstream theorem dAlembert_forces_Jcost, which assembles all structural axioms to conclude that the cost function must be the canonical J-cost. It therefore supplies one link in the chain from the Recognition Composition Law through the eight-tick octave and three-dimensional forcing to the explicit mass ladder. The module records that the d'Alembert equation is the classical continuous solution cosh(λt), here fixed to λ = 1 by the unit calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.