Equation (19) — SDP edge contribution in terms of γ

Proved

QMaxCutSDP.Rounding.eq_19

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

p2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-max-cutsdp-rounding

For a feasible vector solution of (S) and distinct vertices $i,j$ , the normalized correlation $\gamma_{ij}$ and the edge's SDP contribution satisfy

\gamma_{ij}=-\frac{1+v_{ij}\cdot v_0}{2},\qquad (v_0-v_{ij})\cdot v_0=2(1+\gamma_{ij}).

The identity expresses the SDP objective in the same one-edge parameter used to choose the circuit angle.

Formalization Note Feasibility and distinctness make the normalization denominator $2$ , by Lemma 3; no division-by-zero case is imported into the claim.

Preamble

import Mathlib
import Definitions.Def_QMaxCutSDP_Rounding_Model

open Matrix MeasureTheory

Formal statement

namespace QMaxCutSDP.Rounding

/-- Lee, proof of Theorem 1, p. 11, equation (19) and its consequence. -/
theorem eq_19 {n N : ℕ} (v : SDPVec n N) (hv : IsSFeasible v)
    (i j : Fin n) (hij : i ≠ j) :
    gammaE v i j = -(1 + vEdge v i j ⬝ᵥ v.v0) / 2 ∧
    (v.v0 - vEdge v i j) ⬝ᵥ v.v0 = 2 * (1 + gammaE v i j) := by sorry
end QMaxCutSDP.Rounding

Source

Lee, Optimizing quantum circuit parameters via SDP, arXiv:2209.00789v1, p. 11, proof of Theorem 1, eq. (19)

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