HasDAlembert
plain-language theorem explainer
HasDAlembert defines the d'Alembert structure gate for a cost function F by requiring that its shifted log-lift H(t) = F(exp t) + 1 obeys the classical d'Alembert functional equation. Researchers closing the Recognition Science inevitability chain cite it to certify the fourth gate after curvature and symmetry axioms. The definition is a one-line wrapper that applies the SatisfiesDAlembert predicate directly to the exponential lift of F.
Claim. A function $F : ℝ → ℝ$ has d'Alembert structure when the auxiliary map $H(t) := F(e^t) + 1$ satisfies $H(0) = 1$ and $H(t + u) + H(t - u) = 2 H(t) H(u)$ for all real $t, u$.
background
The Fourth Gate module packages the d'Alembert structure condition as a compact certificate in the Recognition Science framework. SatisfiesDAlembert is the predicate that a map H obeys H(0) = 1 together with the functional equation H(t+u) + H(t-u) = 2 H(t) H(u) for all real t and u. In the local setting the module notes that Gate 4 is derived from Gate 3 (curvature) under the Option A formulation: the normalized hyperbolic ODE already forces G(t) = cosh(t) - 1, so the shifted lift H = cosh satisfies d'Alembert automatically. The module therefore supplies a classical functional-equation viewpoint via Aczél's classification theorem whose continuous solutions are exactly cosh(λ t) for λ real.
proof idea
The definition is a one-line wrapper that applies SatisfiesDAlembert to the function (fun t => F (Real.exp t) + 1).
why it matters
This definition completes the fourth gate and feeds the parent theorems dAlembert_forces_Jcost and full_inevitability_four_gates. Those results show that d'Alembert structure together with normalization, symmetry, smoothness and calibration forces F to equal Jcost, thereby closing the four-gate chain to the Recognition Composition Law without extra hypotheses. The downstream summary theorem fourth_gate_summary records that Jcost passes the gate while Fquad fails it, confirming consistency across all four gates in the inevitability equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.