fourth_gate_summary
plain-language theorem explainer
The fourth gate summary establishes that the J-cost satisfies the d'Alembert structure after shifted log-lift while the quadratic counterexample Fquad fails it. Researchers tracing the Recognition Science forcing chain would cite this to confirm the structural filter at gate four. The proof is a direct term conjunction of the affirmative result for Jcost and the refutation for Fquad.
Claim. Let $H(t) = F(e^t) + 1$. Then $H$ satisfies the d'Alembert equation $H(x+y) + H(x-y) = 2H(x)H(y)$ when $F$ is the J-cost, but the corresponding lift fails the equation when $F$ is the quadratic counterexample.
background
The module formalizes the fourth gate as the requirement that the shifted log-lift of a cost function satisfies the classical d'Alembert functional equation. HasDAlembert is defined to hold precisely when this lift meets the equation. The local setting notes that in the Option A formulation, gate four is derived from the curvature gate rather than an independent restriction, serving as a cross-check via Aczél's classification of continuous solutions as hyperbolic cosines.
proof idea
The proof is a term-mode conjunction that directly pairs the theorem establishing d'Alembert structure for the J-cost with the theorem showing its absence for the quadratic counterexample Fquad.
why it matters
This packages the fourth gate verification, confirming that only the J-cost passes the structural filter in the forcing chain. It supports the module's full inevitability claim that d'Alembert structure together with prior axioms forces the cost to be Jcost. The result aligns with J-uniqueness at T5 and the self-similar fixed point at T6 in the Recognition Science landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.