separable_implies_zero_mixed_diff
plain-language theorem explainer
A combiner P that decomposes as P(u,v) = α(u) + β(v) for some α, β yields a vanishing mixed difference at every four points. Workers on the entanglement-gate dichotomy cite the result when separating additive from interactive combiners in the DAlembert setting. The proof extracts the decomposition witness and reduces the four-term expression to zero by direct substitution and ring cancellation.
Claim. If a map $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 quadruple of real numbers $u_0,v_0,u_1,v_1$.
background
The Entanglement Gate module formalizes the cross-derivative test that distinguishes separable from entangling combiners. IsSeparable is the predicate asserting existence of α and β such that P(u,v) equals α(u) plus β(v) for all arguments. The module contrasts this additive case with the RCL combiner 2uv + 2u + 2v, whose mixed second difference equals 2. Upstream structures supply the J-cost and phi-ladder context in which these combiners appear, but the local argument relies only on the algebraic definition of separability.
proof idea
The term-mode proof obtains the witness pair α, β together with the pointwise equality from the separability hypothesis. It then introduces the four evaluation points, substitutes the additive decomposition, and applies the ring tactic to cancel all terms.
why it matters
The lemma supplies the zero-mixed-difference direction required by separable_implies_not_entangling (same module) and by differentiation_key_lemma in AnalyticBridge, which classifies ODE type according to combiner class. It completes the additive half of the gate that separates the RCL interaction term from purely additive forms, thereby anchoring the T5–T6 forcing steps that fix J-uniqueness and the self-similar phi point. No open scaffolding remains for this direction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.