additive_not_entangling
plain-language theorem explainer
The additive combiner Padd(u, v) = 2u + 2v is not entangling, since its mixed second difference vanishes identically at every point. Researchers tracing the four-gate triangulation cite this to exclude the separable branch before the interaction-forces-entanglement step. The proof is a direct term application of the prior Padd_not_entangling result.
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 TriangulatedProof module assembles four gates (interaction, entanglement, curvature, d'Alembert) to reach full inevitability of the J-cost and RCL combiner. The Entanglement Gate defines IsEntangling(P) to mean the mixed second difference is nonzero at some point, equivalently that P cannot be written as α(u) + β(v). The additive combiner Padd is introduced as the explicit separable counterexample Padd(u, v) = 2u + 2v. Upstream Padd_not_entangling already shows the difference is identically zero, and the forces structure from MagnitudeOfMismatch supplies the symmetry context used in the surrounding gates.
proof idea
The proof is a one-line term wrapper that applies the Padd_not_entangling theorem from EntanglementGate.
why it matters
This result excludes the flat additive case inside the triangulation that forces the hyperbolic branch (T5 J-uniqueness) and the RCL combiner. It supplies the concrete non-entangling instance needed to contrast with the RCL case proved entangling in the same module, thereby tightening the path from interaction to the d'Alembert identity and the final unconditional theorem. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.