entanglement_gate_theorem
plain-language theorem explainer
Entanglement gate theorem states that J-cost satisfies the interaction property, the RCL combiner is entangling via nonzero mixed second difference, and the additive combiner is separable. Researchers deriving consistent combiners from the Recognition Composition Law would cite it to confirm interaction is forced. The proof is a one-line term that packages three supporting lemmas.
Claim. The J-cost satisfies HasInteraction, the combiner $P(u,v)=2uv+2u+2v$ is entangling (mixed second difference nonzero at some points), and the combiner $P(u,v)=2u+2v$ is not entangling.
background
The module defines the Entanglement Gate as the requirement that a combiner P has nonzero cross-derivative. IsEntangling(P) holds when the mixed second difference $P(u_1,v_1)-P(u_1,v_0)-P(u_0,v_1)+P(u_0,v_0)$ is nonzero for some points, which for smooth P is equivalent to non-separability. Prcl is the RCL combiner $2uv+2u+2v$ whose mixed difference equals $2(u_1-u_0)(v_1-v_0)$. Padd is the additive combiner $2u+2v$, which is separable as shown by its zero mixed difference. This rests on the NecessityGates result that Jcost has interaction.
proof idea
The proof is a one-line term that refines the conjunction by supplying NecessityGates.Jcost_hasInteraction together with the lemmas Prcl_entangling and Padd_not_entangling.
why it matters
This result shows that any combiner consistent with J must be entangling, and that the RCL combiner satisfies the requirement. It fills the entanglement gate step in the DAlembert foundation, directly supporting the Recognition Composition Law identity. The declaration has no downstream uses yet but closes a necessary link in the forcing chain from J-uniqueness to interaction terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.