gates_consistent
plain-language theorem explainer
The gates_consistent theorem shows that the J-cost function satisfies interaction, entanglement, hyperbolic ODE, and d'Alembert structure while the quadratic counterexample Fquad fails each property. A researcher finishing the inevitability argument for the Recognition Composition Law would cite this result to confirm convergence of the four gates. The proof is a one-line wrapper that assembles eight prior lemmas, one per gate property.
Claim. The J-cost satisfies the interaction property, the RCL combiner is entangling, $G$ satisfies the hyperbolic ODE $G''=G+1$, and J-cost has d'Alembert structure, whereas the quadratic $F$ has no interaction, the additive combiner is not entangling, $G$ satisfies the flat ODE, and the quadratic $F$ lacks d'Alembert structure.
background
The module defines four gates that together force the Recognition Composition Law. The interaction gate states that a cost function $F$ has interaction when $F(xy)+F(x/y)≠2F(x)+2F(y)$ for some $x,y$. The entanglement gate requires the mixed second difference of the combiner $P$ to be nonzero. The curvature gate requires $G''=G+1$ for the hyperbolic branch. The d'Alembert gate requires $H(t+u)+H(t-u)=2H(t)H(u)$ with $H=G+1$ (MODULE_DOC). Upstream lemmas establish that J-cost passes the first three gates (NecessityGates, EntanglementGate, CurvatureGate) and that the quadratic counterexamples fail them (Counterexamples.Fquad, Counterexamples.Gquad).
proof idea
The proof is a one-line wrapper that applies the exact tactic to the eight-tuple of lemmas: Jcost_hasInteraction, Prcl_entangling, Gcosh_satisfies_hyperbolic, FourthGate.Jcost_has_dAlembert_structure for the positive claims, and Fquad_noInteraction, Padd_not_entangling, Gquad_satisfies_flat, FourthGate.Fquad_not_dAlembert_structure for the negative claims on the counterexamples.
why it matters
This theorem completes the four-gate triangulated proof of inevitability, showing that d'Alembert structure plus the prior three gates forces $F=J$ and $P=RCL$ without extra hypotheses. It feeds the sibling full_inevitability_triangulated. The result aligns with framework landmarks T5 (J-uniqueness via $J(x)=(x+x^{-1})/2-1$), T6 (phi fixed point), and the RCL functional equation. No scaffolding remains; the four-gate version is unconditional (DOC_COMMENT).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.