Jcost_has_dAlembert_structure
plain-language theorem explainer
The J-cost function satisfies the d'Alembert functional equation in its shifted log-lift form. Researchers tracing the Recognition Science forcing chain would cite this as the fourth gate verification that confirms the hyperbolic branch. The proof reduces the claim to the known fact that cosh satisfies d'Alembert by showing the log-lift of Jcost equals cosh exactly.
Claim. The cost function $J$ satisfies $H(0)=1$ and $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, where $H(t)=J(e^t)+1$.
background
The Fourth Gate module formalizes the d'Alembert structure condition as a derived property from Gate 3. In the Option A formulation, the curvature gate assumes the ODE $G''(t)=G(t)+1$ together with symmetry and calibration; this forces $G(t)=cosh(t)-1$, so the shifted log-lift $H=G+1=cosh$ automatically satisfies the d'Alembert equation. The definition HasDAlembert F holds precisely when the shifted log-lift $H(t)=F(exp t)+1$ obeys $H(0)=1$ and the functional equation $H(t+u)+H(t-u)=2H(t)H(u)$. Upstream, the theorem cosh_satisfies_dAlembert establishes that the hyperbolic cosine itself satisfies this equation via its addition and subtraction formulas.
proof idea
The proof unfolds HasDAlembert and SatisfiesDAlembert then splits via constructor. The base case $H(0)=1$ follows by simplification using the definition of Jcost and exp zero. The functional equation is handled by first proving the log-lift equals cosh via the cosh identity and exp negation, then applying the theorem cosh_satisfies_dAlembert.
why it matters
This theorem is invoked by fourth_gate_summary to establish that Jcost passes the d'Alembert gate while Fquad does not. It also supports gates_consistent, which verifies that all four gates align on the same conclusion for J versus alternatives. In the framework this confirms the hyperbolic solution at Gate 4, forcing lambda to 1 in the cosh form and completing the classical functional-equation certificate path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.