separable_implies_zero_mixed_diff

formal source

 102/-! ## Separability is Equivalent to Zero Mixed Difference -/
 103
 104/-- Separable implies zero mixed difference. -/
 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
 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). -/
 113theorem separable_implies_not_entangling (P : ℝ → ℝ → ℝ) (hSep : IsSeparable P) :
 114    ¬ IsEntangling P := by
 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. -/
 122theorem separable_with_boundary_is_additive (P : ℝ → ℝ → ℝ)
 123    (hSep : IsSeparable P)
 124    (hBdryU : ∀ u, P u 0 = 2 * u)
 125    (hBdryV : ∀ v, P 0 v = 2 * v) :
 126    ∀ u v, P u v = 2 * u + 2 * v := by
 127  obtain ⟨α, β, hαβ⟩ := hSep
 128  -- From hBdryU: α(u) + β(0) = 2u, so α(u) = 2u - β(0)
 129  have hα : ∀ u, α u = 2 * u - β 0 := by
 130    intro u
 131    have := hBdryU u
 132    rw [hαβ] at this
 133    linarith
 134  -- From hBdryV: α(0) + β(v) = 2v, so β(v) = 2v - α(0)
 135  have hβ : ∀ v, β v = 2 * v - α 0 := by