separable_implies_zero_mixed_diff
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.
claimIf 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 in Recognition Science
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.
scope and limits
- Does not establish the converse for entangling combiners.
- Does not assume or derive any differentiability of P.
- Does not quantify the magnitude of the mixed difference when separability fails.
- Does not connect the result to specific constants such as alpha or G.
Lean usage
example (P : ℝ → ℝ → ℝ) (hSep : IsSeparable P) (u0 v0 u1 v1 : ℝ) : P u1 v1 - P u1 v0 - P u0 v1 + P u0 v0 = 0 := separable_implies_zero_mixed_diff P hSep u0 v0 u1 v1formal statement (Lean)
105theorem separable_implies_zero_mixed_diff (P : ℝ → ℝ → ℝ) (hSep : IsSeparable P) :
106 ∀ u₀ v₀ u₁ v₁, P u₁ v₁ - P u₁ v₀ - P u₀ v₁ + P u₀ v₀ = 0 := by
proof body
Term-mode proof.
107 obtain ⟨α, β, h⟩ := hSep
108 intro u₀ v₀ u₁ v₁
109 simp only [h]
110 ring
111
112/-- Separable implies not entangling (contrapositive of entangling implies not separable). -/