Lemma 8, p. 22 — if M(p, q, r) ⪰ 0 and q ≤ 0, then p ≥ −√3/2
ProvedQMCProduct.HalfApprox.lemma_8monogamy-of-entanglementp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-informationsemidefinite-programming
Let be the real SWAP Gram matrix displayed in Section 4.3. If is positive semidefinite and , then
The bound rules out a sufficiently negative SWAP value on one edge alongside a nonpositive value on an adjacent edge.
Formalization Note The statement follows the printed lemma. The proof's displayed dual certificate has a coordinate-order erratum, recorded in the moderation notes.
Preamble
import Definitions.Def_QMCProduct_HalfApprox_Basic set_option autoImplicit false
Formal statement
namespace QMCProduct.HalfApprox
/-- Lemma 8, p. 22. -/
theorem lemma_8 (p q r : ℝ) (hM : (swapGram p q r).PosSemidef) (hq : q ≤ 0) :
-(Real.sqrt 3) / 2 ≤ p := by sorry
end QMCProduct.HalfApprox
Source
Parekh & Thompson, An Optimal Product-State Approximation for 2-Local Quantum Hamiltonians with Positive Terms, arXiv:2206.08342v2, p. 22, Lemma 8
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.