separable_implies_not_entangling
plain-language theorem explainer
If a combiner P is separable then it cannot be entangling. Researchers modeling interaction gates in the D'Alembert layer cite this result to separate the additive combiner from the RCL form that carries a nonzero cross term. The proof is a one-line wrapper that feeds the entangling witness points into the zero-mixed-difference lemma and obtains an immediate contradiction.
Claim. Let $P : ℝ → ℝ → ℝ$. If $P$ is separable, i.e., there exist functions $α, β : ℝ → ℝ$ such that $P(u,v) = α(u) + β(v)$ for all real $u,v$, then $P$ is not entangling: there do not 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 Entanglement Gate module characterizes combiners by cross-derivative behavior. A combiner is separable when it decomposes as $P(u,v) = α(u) + β(v)$ for some functions α and β. It is entangling when the mixed second difference is nonzero at some quadruple of points. The upstream lemma separable_implies_zero_mixed_diff shows that any separable P forces this difference to vanish identically, proved by substituting the decomposition and simplifying with ring tactics.
proof idea
The proof proceeds by contradiction. Assume IsEntangling P, which supplies concrete points u0,v0,u1,v1 at which the mixed difference is nonzero. Apply the lemma separable_implies_zero_mixed_diff P hSep to those same points; the difference must then be zero. This contradicts the witness, discharging the assumption.
why it matters
The theorem separates the additive combiner (zero cross term) from the RCL combiner (nonzero cross term 2uv) inside the Entanglement Gate. It thereby supports the physical reading that composite observations introduce genuine coupling rather than mere addition. In the Recognition Science setting it reinforces the interaction requirement that appears in the forcing chain after J-uniqueness and before the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.