Lemma 3 — identities for feasible SDP vectors

Proved

QMaxCutSDP.Rounding.lemma_3

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-max-cutsemidefinite-programming

For a feasible solution of (S), put $v_{ij}=\sum_{a=1}^3v_{ij,a}$ . For distinct vertices $i,j$ , and for pairwise distinct $i,j,k$ in the last identity,

\|v_{ij}\|^2=3-2v_{ij}\cdot v_0,\qquad \|v_0+v_{ij}\|^2=4,\qquad v_{ij}\cdot v_{jk}=v_{ik}\cdot v_0.

The fixed norm of $v_0+v_{ij}$ makes the normalized edge correlation well-defined on actual edges.

Formalization Note Distinctness is explicit because the constraints of (S) impose these relations only on distinct indices.

Preamble

import Mathlib
import Definitions.Def_QMaxCutSDP_Rounding_Model

open Matrix MeasureTheory

Formal statement

namespace QMaxCutSDP.Rounding

/-- Lee, Lemma 3, p. 7, equations (10)–(12). -/
theorem lemma_3 {n N : ℕ} (v : SDPVec n N) (hv : IsSFeasible v) :
    (∀ i j : Fin n, i ≠ j →
      (vEdge v i j ⬝ᵥ vEdge v i j = 3 - 2 * (vEdge v i j ⬝ᵥ v.v0)) ∧
      ((v.v0 + vEdge v i j) ⬝ᵥ (v.v0 + vEdge v i j) = 4)) ∧
    (∀ i j k : Fin n, i ≠ j → j ≠ k → i ≠ k →
      vEdge v i j ⬝ᵥ vEdge v j k = vEdge v i k ⬝ᵥ v.v0) := by sorry
end QMaxCutSDP.Rounding

Source

Lee, Optimizing quantum circuit parameters via SDP, arXiv:2209.00789v1, p. 7, Lemma 3, eqs. (9)–(12)

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph