separable_implies_zero_mixed_diff
plain-language theorem explainer
A combiner P that decomposes as the sum of a function of its first argument alone and a function of its second argument alone produces a vanishing mixed second difference at every four points. Researchers formalizing the entanglement gate cite the result to separate additive from interactive combiners before invoking smoothness or ODE consequences. The proof obtains the two witnessing functions from the separability hypothesis and reduces the four-term difference to zero by ring cancellation.
Claim. If a function $P : ℝ → ℝ → ℝ$ admits functions $α, β$ such that $P(u,v) = α(u) + β(v)$ for all real $u,v$, then $P(u_1,v_1) - P(u_1,v_0) - P(u_0,v_1) + P(u_0,v_0) = 0$ holds for every choice of real numbers $u_0,v_0,u_1,v_1$.
background
The Entanglement Gate module characterizes combiners by the presence or absence of a nonzero mixed second difference, which under smoothness is equivalent to a nonzero cross derivative. Separability means the combiner splits into independent contributions from each variable, exactly the additive form that produces zero cross term. This stands in direct contrast to the RCL combiner whose 2uv term supplies the interaction that defines entanglement.
proof idea
The term proof extracts the pair of functions witnessing separability, substitutes the additive decomposition into the mixed difference, and invokes ring to cancel all four terms identically.
why it matters
The result supplies the zero mixed-difference fact used by the contrapositive theorem that separable combiners are not entangling and by the differentiation key lemma that maps combiner type to ODE type. It therefore marks the boundary between additive and interactive regimes at the foundation level, prior to the introduction of the phi-ladder or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.