Prcl
plain-language theorem explainer
The RCL combiner is the function P(u, v) = 2uv + 2u + 2v. Researchers on the entanglement gate cite this definition to distinguish the J-cost combiner from separable alternatives. It is introduced as a direct definition matching the bilinear cross term in the Recognition Composition Law.
Claim. Let $P(u, v) := 2uv + 2u + 2v$ be the RCL combiner function on real arguments.
background
The Entanglement Gate module requires that a combiner P have nonzero mixed second difference to encode interaction between its arguments, as opposed to separability. The RCL combiner is the explicit bilinear form P(u, v) = 2uv + 2u + 2v that reproduces the cross term in the Recognition Composition Law. Upstream results include the structure of J-cost minimization (strictly convex with unique minimum at argument 1) from PhysicsComplexityStructure.of and the phi-forcing structure from PhiForcingDerived.of.
proof idea
This declaration is a direct definition of the combiner as the expression 2uv + 2u + 2v.
why it matters
This definition supplies the entangling combiner referenced in entanglement_gate_theorem (which asserts J has interaction and therefore requires an entangling rather than additive combiner) and in gates_connected (which chains interaction to hyperbolic curvature and d'Alembert). It realizes the Recognition Composition Law at the level of the entanglement gate and appears in the triangulated consistency result that J passes all four gates while quadratic alternatives fail. It closes the step from J-uniqueness in the forcing chain to the nonzero cross-derivative requirement for composite observations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.