HasDAlembert
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove that any concrete F satisfies the predicate.
- Does not derive the explicit solution form cosh(λ t).
- Does not link the predicate to the curvature ODE or prior gates.
- Does not treat discrete or non-smooth cost functions.
formal statement (Lean)
49def HasDAlembert (F : ℝ → ℝ) : Prop :=
proof body
Definition body.
50 SatisfiesDAlembert (fun t => F (Real.exp t) + 1)
51
52/-! ## Canonical Solutions -/
53
54/-- cosh satisfies the d'Alembert equation. -/