Prcl_entangling
plain-language theorem explainer
The RCL combiner satisfies the entanglement condition because its mixed second difference evaluates to 2 at the witness points (0,0) and (1,1). Researchers tracing the d'Alembert gates or the interaction-to-entanglement step in Recognition Science would cite this result to confirm that the 2uv term forces non-separability. The proof is a one-line witness application of the mixed-difference identity for Prcl followed by norm_num evaluation.
Claim. Let $P(u,v) = 2uv + 2u + 2v$ be the RCL combiner. Then $P$ is entangling: there 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) = 2(u_1 - u_0)(v_1 - v_0) = 2$ when the points are $(0,0)$ and $(1,1)$.
background
The Entanglement Gate module defines a combiner $P$ to be entangling when it is not separable as a sum of independent functions of each argument. Equivalently, 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 choice of points. Prcl is the concrete RCL combiner $2uv + 2u + 2v$ that encodes the Recognition Composition Law. The upstream lemma Prcl_mixed_diff states that this difference equals exactly $2(u_1 - u_0)(v_1 - v_0)$, so any distinct pairs immediately give a nonzero value. The module doc notes that entanglement captures the physical statement that observing a composite system $xy$ is not merely the sum of observations on $x$ and $y$ separately; the interaction term $2uv$ supplies the coupling.
proof idea
The term-mode proof supplies the explicit witness $(0,0,1,1)$ to the existential in IsEntangling, rewrites the mixed difference via the upstream identity Prcl_mixed_diff, and reduces the resulting expression $2(1-0)(1-0)$ by norm_num to obtain the nonzero value 2.
why it matters
Prcl_entangling is invoked directly by entanglement_gate_theorem (which pairs it with Jcost_hasInteraction and Padd_not_entangling) and by the three consistency results in TriangulatedProof: gates_connected, gates_consistent, and gates_equivalent_for_Jcost. It therefore closes the second gate in the four-gate triangulation that forces the Recognition Composition Law to be the unique entangling combiner compatible with J-cost. The result sits inside the T5–T6 forcing chain: J-uniqueness plus the RCL identity together require the interaction term that produces nonzero cross-derivative, which in turn selects the hyperbolic ODE solved by the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.