pith. machine review for the scientific record. sign in
theorem proved term proof high

RCL_is_entangling

show as:
view Lean formalization →

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).

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  95theorem RCL_is_entangling : IsEntangling Prcl := Prcl_entangling

proof body

Term-mode proof.

  96
  97/-- Additive combiner is not entangling. -/

depends on (7)

Lean names referenced from this declaration's body.