separable_implies_not_entangling
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the converse (entangling implies not separable).
- Does not quantify the magnitude of any nonzero cross term.
- Does not address non-smooth or discrete combiners.
- Does not link the gate to specific constants such as phi or alpha.
formal statement (Lean)
113theorem separable_implies_not_entangling (P : ℝ → ℝ → ℝ) (hSep : IsSeparable P) :
114 ¬ IsEntangling P := by
proof body
Term-mode proof.
115 intro ⟨u₀, v₀, u₁, v₁, h⟩
116 exact h (separable_implies_zero_mixed_diff P hSep u₀ v₀ u₁ v₁)
117
118/-! ## Connection to the F-level Interaction Gate -/
119
120/-- If P is separable AND satisfies both boundary conditions,
121 then P must be the additive combiner 2u + 2v. -/