separable_implies_not_entangling

formal source

 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
 136    intro v
 137    have := hBdryV v
 138    rw [hαβ] at this
 139    linarith
 140  -- From hα at u=0: α(0) = -β(0)
 141  have hα0 : α 0 = -β 0 := by
 142    have := hα 0
 143    simp at this