Padd_not_entangling
plain-language theorem explainer
The additive combiner P(u,v) = 2u + 2v is separable and therefore not entangling. Researchers working on the d'Alembert gates cite this to rule out additive rules when interaction is required. The proof is a one-line contradiction that applies the lemma establishing the mixed second difference vanishes identically.
Claim. Let $P(u,v) := 2u + 2v$. Then there do not exist $u_0,v_0,u_1,v_1$ such that $P(u_1,v_1) - P(u_1,v_0) - P(u_0,v_1) + P(u_0,v_0) ≠ 0$.
background
The Entanglement Gate module defines a combiner P as entangling precisely when the mixed second difference is nonzero at some quadruple of points, which is equivalent to P not being separable into α(u) + β(v). The additive combiner is introduced as the canonical separable case with P(u,v) = 2u + 2v. The module contrasts this with the RCL combiner that carries the interaction term 2uv. The upstream lemma Padd_mixed_diff_zero states that the mixed difference for this P vanishes for every choice of arguments.
proof idea
Assume IsEntangling Padd. This supplies witnesses u0,v0,u1,v1 together with a nonzero mixed difference. The proof applies the lemma that this mixed difference is identically zero, producing an immediate contradiction.
why it matters
The result is invoked inside the Entanglement Gate Theorem to establish that any combiner consistent with J-cost interaction must be entangling, thereby excluding the additive rule. It appears as one of the four gates inside the Triangulated Proof that together confirm J passes while Fquad fails. The gate directly encodes the requirement that the Recognition Science combiner must contain the 2uv interaction term of the RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.