Prcl_mixed_diff
plain-language theorem explainer
The mixed second difference of the RCL combiner equals twice the product of the increments in each argument. Researchers formalizing the entanglement gate in the DAlembert setting cite this identity to separate entangling from separable combiners. The proof is a direct algebraic expansion that substitutes the combiner definition and normalizes via the ring tactic.
Claim. Let $P(u,v) = 2uv + 2u + 2v$. Then for all real $u_0,v_0,u_1,v_1$, $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)$.
background
The Entanglement Gate module requires that a combiner $P$ have nonzero cross-derivative, distinguishing interaction from additivity. The RCL combiner is defined by $P(u,v) := 2uv + 2u + 2v$, which supplies the interaction term $2uv$ that appears in the Recognition Composition Law. The module notes that entanglement means observation of the composite $xy$ is not merely the sum of separate observations of $x$ and $y$. Upstream results supply the definition of this combiner together with auxiliary statements on collision-free programs and edge lengths, though the present identity uses only the definition itself.
proof idea
The proof introduces the four real variables, substitutes the explicit definition of the combiner, and invokes the ring tactic to expand the left-hand side and cancel all terms except the desired product $2(u_1-u_0)(v_1-v_0)$.
why it matters
The identity is invoked by the sibling theorems Prcl_entangling and Prcl_not_separable, and by the downstream result entangling_with_boundary_is_RCL, which states that any entangling combiner satisfying the boundary conditions $P(u,0)=2u$ and $P(0,v)=2v$ must coincide with the RCL form. It therefore supplies the concrete cross-derivative witness that realizes the Entanglement Gate characterization inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.