Matrix Sum-of-Squares Helpers

This module contains finite-dimensional complex matrix lemmas used by the EPR extraction arguments. It is intentionally concrete over complex matrices: the proofs use Matrix.dotProduct positivity and conjugate transpose.

theorem MIPRE.LCS.three_nonneg_add_eq_zero {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c : α} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a + b + c = 0) : a = 0 ∧ b = 0 ∧ c = 0

theorem MIPRE.LCS.dotProduct_square_mulVec_eq_dotProduct_mulVec_self {m : Type u_1} [Fintype m] [DecidableEq m] (T : Matrix m m ℂ) (v : m → ℂ) (hT : T.conjTranspose = T) : star v ⬝ᵥ (T ^ 2).mulVec v = star (T.mulVec v) ⬝ᵥ T.mulVec v

theorem MIPRE.LCS.three_selfAdjoint_squares_mulVec_eq_zero {m : Type u_1} [Fintype m] [DecidableEq m] (T₁ T₂ T₃ : Matrix m m ℂ) (v : m → ℂ) (hT₁ : T₁.conjTranspose = T₁) (hT₂ : T₂.conjTranspose = T₂) (hT₃ : T₃.conjTranspose = T₃) (h : (T₁ ^ 2 + T₂ ^ 2 + T₃ ^ 2).mulVec v = 0) : T₁.mulVec v = 0 ∧ T₂.mulVec v = 0 ∧ T₃.mulVec v = 0