RCL_is_entangling
plain-language theorem explainer
The RCL combiner P(u,v) = 2uv + 2u + 2v satisfies the entangling condition that its mixed second difference is nonzero at some points. Researchers tracing the Recognition Science forcing chain cite this to establish non-separability after the interaction gate. The proof is a one-line wrapper that applies the explicit witness theorem supplying points (0,0) and (1,1).
Claim. The combiner defined by $P(u,v) = 2uv + 2u + 2v$ is entangling: there exist real numbers $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 to reach full inevitability. The entanglement gate defines a combiner as entangling precisely when it fails to be separable into α(u) + β(v), equivalently when the mixed second difference is nonzero somewhere. The RCL combiner is the explicit function 2uv + 2u + 2v.
proof idea
One-line wrapper that applies the Prcl_entangling theorem, which exhibits the witness points (0,0) and (1,1) and reduces the mixed difference via the mixed-diff identity to a direct numerical check of 2.
why it matters
This step confirms the RCL combiner is entangling and feeds the full_inevitability_triangulated result. It fills the explicit line 'RCL combiner is entangling' in the four-gate structure, closing the path from interaction to the hyperbolic solution G = cosh - 1. In the Recognition Science framework it supports J-uniqueness via the composition law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.