pith. machine review for the scientific record. sign in
theorem proved term proof high

gates_consistent

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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).

scope and limits

formal statement (Lean)

 199theorem gates_consistent :
 200    -- J has all four properties
 201    HasInteraction Cost.Jcost ∧
 202    IsEntangling Prcl ∧
 203    SatisfiesHyperbolicODE Gcosh ∧
 204    FourthGate.HasDAlembert Cost.Jcost ∧
 205    -- Fquad/Padd have the opposite properties
 206    ¬ HasInteraction Counterexamples.Fquad ∧
 207    ¬ IsEntangling Padd ∧
 208    SatisfiesFlatODE Gquad ∧
 209    ¬ FourthGate.HasDAlembert Counterexamples.Fquad := by

proof body

Term-mode proof.

 210  exact ⟨Jcost_hasInteraction, Prcl_entangling, Gcosh_satisfies_hyperbolic,
 211         FourthGate.Jcost_has_dAlembert_structure,
 212         Fquad_noInteraction, Padd_not_entangling, Gquad_satisfies_flat,
 213         FourthGate.Fquad_not_dAlembert_structure⟩
 214
 215/-! ## Complete Inevitability with Four Gates -/
 216
 217/-- **Full Inevitability with Four Gates**: d'Alembert structure completes the proof.
 218
 219    Unlike the three-gate version which required a bridge hypothesis,
 220    the four-gate version is fully proved:
 221
 222    d'Alembert structure + structural axioms ⟹ F = J ⟹ P = RCL
 223-/

depends on (35)

Lean names referenced from this declaration's body.

… and 5 more