Exact certificates for upper bounds on the commuting-operator value

Step §3.5 of the Tsirelson route (planning/tsirelson-campaign.md): finite certificates, with Gaussian-integer coefficients and an exact test, for strict upper bounds on the commuting-operator value of a game, at the level of the game algebra NCPoly (Gen X Y A B). The coded layer only has to show that its checker computes this test on decoded data.

Certificates. Fix κ > 0; the coded layer takes κ = q·W_d and r = p/q, so that κ r·1 - κ W_G has Gaussian-integer coefficients. A certificate is a scale N ≥ 1, a list σ of hermitian squares (g, s) standing for s⋆ g s, with g = none read as 1 (sosPoly), and a list ι of ideal monomials (c, w, ρ, w') standing for c · w ρ w', with w, w' words and ρ ∈ rels X Y A B (idealPoly), all with Gaussian-integer coefficients. The test is that the hermitian part T + T⋆ of the residual

T = N² (κ r·1 - κ W_G) - Σ s⋆ g s - Σ c · w ρ w'

is dominant (Dominant): the real part of its constant coefficient strictly exceeds the taxicab mass Σ_{w ≠ 1} (|Re z_w| + |Im z_w|) of its other coefficients.

Soundness (commutingOperatorValue_lt_of_dominant, commutingOperatorValue_lt_of_certificate). Every word evaluates to a contraction, so the state φ of a strategy satisfies Re φ(z) ≥ Re z_1 - Σ_{w ≠ 1} (|Re z_w| + |Im z_w|) (re_map_ge_of_norm_le, re_inner_eval_ge). The state is hermitian, nonnegative on hermitian squares, and zero on the relation ideal, so Re φ(T + T⋆) = 2 Re φ(T) ≤ 2κ (r - value). The dominance margin δ of T + T⋆ depends only on T, so every strategy has value at most r - δ / (2κ), and so does the supremum (ciSup_le, which needs a strategy: the answer sets are nonempty).

Completeness (exists_certificate_of_lt). Take value < r' < r. The Positivstellensatz puts κ (r'·1 - W_G) in the cone M, and every element of M is Σ s⋆ g s + j + a with j in the relation ideal and a anti-hermitian (exists_decomp_of_mem_qmod), where j = Σ c · w ρ w' (exists_idealPoly_eq_of_mem_relSpan). So

κ r·1 - κ W_G = ε·1 + Σ s⋆ g s + Σ c · w ρ w' + a, ε = κ (r - r') > 0.

Round the coefficients of every N s and every N² c to Gaussian integers (roundPoly, roundC), with taxicab error at most 1 per coefficient (abs_sub_round). The residual is then T = N² ε·1 + N² a + E, where the rounding error satisfies ‖E‖₁ ≤ N C for a constant C of the decomposition (l1_sq_smul_sosPoly_sub_le, l1_sq_smul_idealPoly_sub_le: the ℓ¹ norm NCPoly.l1 is subadditive, submultiplicative and invariant under the star). Symmetrizing kills N² a: T + T⋆ = 2 N² ε·1 + (E + E⋆), which is dominant as soon as 2 N C < 2 N² ε (dominant_smul_one_add), that is for N > C / ε. Completeness needs no integrality of κ r·1 - κ W_G; that hypothesis is what makes the certificate encodable.

Together: for nonempty answer sets and any κ > 0, the value is below r exactly when a certificate exists (exists_certificate_iff).

Dominant is defined with classical decidable equality of words; dominant_iff and dominant_iff_of_subset restate it for any decidable equality, and as a sum over the nonempty words of any finite set containing the support, which is the form the coded checker computes.

Main declarations

• sosPoly, idealPoly, sosPoly_mem_qmod, idealPoly_mem_relSpan, exists_idealPoly_eq_of_mem_relSpan, exists_decomp_of_mem_qmod;
• Dominant, dominant_iff, dominant_iff_of_subset, dominant_iff_l1, dominant_smul_one_add, re_map_ge_of_norm_le;
• roundC, roundPoly, roundSos, roundIdeal, l1_sq_smul_sub_roundPoly_le, l1_sq_smul_sub_roundC_le, l1_sq_smul_sosPoly_sub_le, l1_sq_smul_idealPoly_sub_le;
• re_inner_eval_ge, commutingOperatorValue_lt_of_dominant, commutingOperatorValue_lt_of_certificate, exists_certificate_of_lt, exists_certificate_iff.

Sums of squares and ideal monomials

noncomputable def MIPRE.Tsirelson.sosPoly {G : Type u_1} (σ : List (Option G × NCPoly G)) : NCPoly G

The sum of hermitian squares Σ s⋆ g s of a list of terms (g, s), where g = none stands for 1 and g = some g' for the letter g'.

Equations

• MIPRE.Tsirelson.sosPoly σ = (List.map (fun (p : Option G × MIPRE.NCPoly G) => star p.2 * p.1.elim 1 MIPRE.NCPoly.gen * p.2) σ).sum

noncomputable def MIPRE.Tsirelson.idealPoly {G : Type u_1} {R : Set (NCPoly G)} (ι : List (ℂ × FreeMonoid G × { ρ : NCPoly G // ρ ∈ R } × FreeMonoid G)) : NCPoly G

The element Σ c · w ρ w' of the relation ideal of a list of ideal monomials (c, w, ρ, w'): a scalar, two words, and a relation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Tsirelson.sosPoly_nil {G : Type u_1} : sosPoly [] = 0

The empty sum of hermitian squares.

@[simp]

theorem MIPRE.Tsirelson.sosPoly_cons {G : Type u_1} (p : Option G × NCPoly G) (σ : List (Option G × NCPoly G)) : sosPoly (p :: σ) = star p.2 * p.1.elim 1 NCPoly.gen * p.2 + sosPoly σ

A sum of hermitian squares, one term at a time.

@[simp]

theorem MIPRE.Tsirelson.sosPoly_append {G : Type u_1} (σ σ' : List (Option G × NCPoly G)) : sosPoly (σ ++ σ') = sosPoly σ + sosPoly σ'

Sums of hermitian squares add under concatenation.

@[simp]

theorem MIPRE.Tsirelson.idealPoly_nil {G : Type u_1} {R : Set (NCPoly G)} : idealPoly [] = 0

The empty combination of ideal monomials.

@[simp]

theorem MIPRE.Tsirelson.idealPoly_cons {G : Type u_1} {R : Set (NCPoly G)} (t : ℂ × FreeMonoid G × { ρ : NCPoly G // ρ ∈ R } × FreeMonoid G) (ι : List (ℂ × FreeMonoid G × { ρ : NCPoly G // ρ ∈ R } × FreeMonoid G)) : idealPoly (t :: ι) = t.1 • (NCPoly.single t.2.1 1 * ↑t.2.2.1 * NCPoly.single t.2.2.2 1) + idealPoly ι

A combination of ideal monomials, one term at a time.

@[simp]

theorem MIPRE.Tsirelson.idealPoly_append {G : Type u_1} {R : Set (NCPoly G)} (ι ι' : List (ℂ × FreeMonoid G × { ρ : NCPoly G // ρ ∈ R } × FreeMonoid G)) : idealPoly (ι ++ ι') = idealPoly ι + idealPoly ι'

Combinations of ideal monomials add under concatenation.

theorem MIPRE.Tsirelson.star_mul_elim_mul_mem_qmod {G : Type u_1} {R : Set (NCPoly G)} (s : NCPoly G) (g : Option G) : star s * g.elim 1 NCPoly.gen * s ∈ NCPoly.qmod R

The hermitian square s⋆ g s lies in the quadratic module.

theorem MIPRE.Tsirelson.sosPoly_mem_qmod {G : Type u_1} {R : Set (NCPoly G)} (σ : List (Option G × NCPoly G)) : sosPoly σ ∈ NCPoly.qmod R

A sum of hermitian squares lies in the quadratic module.

theorem MIPRE.Tsirelson.idealPoly_mem_relSpan {G : Type u_1} {R : Set (NCPoly G)} (ι : List (ℂ × FreeMonoid G × { ρ : NCPoly G // ρ ∈ R } × FreeMonoid G)) : idealPoly ι ∈ NCPoly.relSpan R

A combination of ideal monomials lies in the relation ideal.

theorem MIPRE.Tsirelson.idealPoly_map_mul {G : Type u_1} {R : Set (NCPoly G)} (c : ℂ) (ι : List (ℂ × FreeMonoid G × { ρ : NCPoly G // ρ ∈ R } × FreeMonoid G)) : idealPoly (List.map (fun (t : ℂ × FreeMonoid G × { ρ : NCPoly G // ρ ∈ R } × FreeMonoid G) => (c * t.1, t.2)) ι) = c • idealPoly ι

Scaling the scalars of a list of ideal monomials.

theorem MIPRE.Tsirelson.sosPoly_map_smul {G : Type u_1} (c : ℂ) (σ : List (Option G × NCPoly G)) : sosPoly (List.map (fun (p : Option G × NCPoly G) => (p.1, c • p.2)) σ) = ((starRingEnd ℂ) c * c) • sosPoly σ

Scaling the vectors of a list of hermitian squares.

theorem MIPRE.Tsirelson.exists_idealPoly_eq_mul_mul {G : Type u_1} {R : Set (NCPoly G)} (u : NCPoly G) {ρ : NCPoly G} (hρ : ρ ∈ R) (v : NCPoly G) : ∃ (ι : List (ℂ × FreeMonoid G × { ρ : NCPoly G // ρ ∈ R } × FreeMonoid G)), idealPoly ι = u * ρ * v

Every u ρ v is a combination of ideal monomials c · w ρ w'.

theorem MIPRE.Tsirelson.exists_idealPoly_eq_of_mem_relSpan {G : Type u_1} {R : Set (NCPoly G)} {j : NCPoly G} (hj : j ∈ NCPoly.relSpan R) : ∃ (ι : List (ℂ × FreeMonoid G × { ρ : NCPoly G // ρ ∈ R } × FreeMonoid G)), idealPoly ι = j

Monomial decomposition of the relation ideal. Every element of the relation ideal is a finite combination of ideal monomials c · w ρ w', with w, w' words and ρ ∈ R.

theorem MIPRE.Tsirelson.exists_decomp_of_mem_qmod {G : Type u_1} {R : Set (NCPoly G)} {m : NCPoly G} (hm : m ∈ NCPoly.qmod R) : ∃ (σ : List (Option G × NCPoly G)) (j : NCPoly G) (a : NCPoly G), j ∈ NCPoly.relSpan R ∧ star a = -a ∧ m = sosPoly σ + j + a

Decomposition of the quadratic module. Every element of qmod R is a sum of hermitian squares s⋆ g s, an element of the relation ideal, and an anti-hermitian element.

Dominance

def MIPRE.Tsirelson.Dominant {G : Type u_1} (z : NCPoly G) : Prop

A polynomial is dominant if the real part of its constant coefficient strictly exceeds the taxicab mass of its other coefficients: Σ_{w ≠ 1} (|Re z_w| + |Im z_w|) < Re z_1.

Equations

• MIPRE.Tsirelson.Dominant z = (∑ w ∈ z.coeff.support.erase 1, (|(z.coeff w).re| + |(z.coeff w).im|) < (z.coeff 1).re)

theorem MIPRE.Tsirelson.sum_erase_one_eq_of_subset {G : Type u_1} [DecidableEq (FreeMonoid G)] (z : NCPoly G) {s : Finset (FreeMonoid G)} (hs : z.coeff.support ⊆ s) : ∑ w ∈ z.coeff.support.erase 1, (|(z.coeff w).re| + |(z.coeff w).im|) = ∑ w ∈ s.erase 1, (|(z.coeff w).re| + |(z.coeff w).im|)

The off-unit mass as a sum over the nonempty words of any finite set of words containing the support.

theorem MIPRE.Tsirelson.dominant_iff_of_subset {G : Type u_1} [DecidableEq (FreeMonoid G)] (z : NCPoly G) {s : Finset (FreeMonoid G)} (hs : z.coeff.support ⊆ s) : Dominant z ↔ ∑ w ∈ s.erase 1, (|(z.coeff w).re| + |(z.coeff w).im|) < (z.coeff 1).re

Dominance, over the nonempty words of any finite set of words containing the support.

theorem MIPRE.Tsirelson.dominant_iff {G : Type u_1} [DecidableEq (FreeMonoid G)] (z : NCPoly G) : Dominant z ↔ ∑ w ∈ z.coeff.support.erase 1, (|(z.coeff w).re| + |(z.coeff w).im|) < (z.coeff 1).re

Dominance, for any decidable equality on words.

theorem MIPRE.Tsirelson.l1_eq_add_sum_erase_one {G : Type u_1} [DecidableEq (FreeMonoid G)] (z : NCPoly G) : z.l1 = |(z.coeff 1).re| + |(z.coeff 1).im| + ∑ w ∈ z.coeff.support.erase 1, (|(z.coeff w).re| + |(z.coeff w).im|)

The ℓ¹ norm splits into the constant coefficient and the off-unit mass.

theorem MIPRE.Tsirelson.dominant_iff_l1 {G : Type u_1} (z : NCPoly G) : Dominant z ↔ z.l1 < (z.coeff 1).re + (|(z.coeff 1).re| + |(z.coeff 1).im|)

Dominance in terms of the ℓ¹ norm.

theorem MIPRE.Tsirelson.dominant_smul_one_add {G : Type u_1} {c : ℝ} {e : NCPoly G} (h : e.l1 < c) : Dominant (↑c • 1 + e)

A perturbation of a positive multiple of the unit is dominant: if ‖e‖₁ < c, then c·1 + e is dominant.

theorem MIPRE.Tsirelson.re_map_ge_of_norm_le {G : Type u_1} [DecidableEq (FreeMonoid G)] (L : NCPoly G →ₗ[ℂ] ℂ) (h1 : L 1 = 1) (hw : ∀ (w : FreeMonoid G), ‖L (NCPoly.single w 1)‖ ≤ 1) (z : NCPoly G) : (z.coeff 1).re - ∑ w ∈ z.coeff.support.erase 1, (|(z.coeff w).re| + |(z.coeff w).im|) ≤ (L z).re

The dominance margin bounds every normalized functional that is bounded by 1 on words. For a ℂ-linear functional L with L 1 = 1 and ‖L w‖ ≤ 1 on every word, Re L z ≥ Re z_1 - Σ_{w ≠ 1} (|Re z_w| + |Im z_w|); in particular Re L z > 0 when z is dominant.

Rounding to Gaussian integers

noncomputable def MIPRE.Tsirelson.roundC (z : ℂ) : ℂ

Rounding a complex number to a nearest Gaussian integer, coordinatewise.

Equations

• MIPRE.Tsirelson.roundC z = ↑(round z.re) + ↑(round z.im) * Complex.I

theorem MIPRE.Tsirelson.exists_roundC_eq (z : ℂ) : ∃ (m : ℤ) (n : ℤ), roundC z = ↑m + ↑n * Complex.I

A rounded complex number is a Gaussian integer.

@[simp]

theorem MIPRE.Tsirelson.roundC_zero : roundC 0 = 0

Rounding fixes 0.

theorem MIPRE.Tsirelson.abs_re_add_abs_im_roundC_sub_le (z : ℂ) : |(roundC z - z).re| + |(roundC z - z).im| ≤ 1

The rounding error of a complex number has taxicab norm at most 1.

noncomputable def MIPRE.Tsirelson.roundPoly {G : Type u_1} (s : NCPoly G) : NCPoly G

Rounding a polynomial coefficientwise to Gaussian integers.

Equations

• MIPRE.Tsirelson.roundPoly s = MIPRE.NCPoly.ofCoeff (Finsupp.mapRange MIPRE.Tsirelson.roundC MIPRE.Tsirelson.roundC_zero s.coeff)

@[simp]

theorem MIPRE.Tsirelson.coeff_roundPoly {G : Type u_1} (s : NCPoly G) (w : FreeMonoid G) : (roundPoly s).coeff w = roundC (s.coeff w)

The coefficients of a rounded polynomial.

theorem MIPRE.Tsirelson.exists_coeff_roundPoly_eq {G : Type u_1} (s : NCPoly G) (w : FreeMonoid G) : ∃ (m : ℤ) (n : ℤ), (roundPoly s).coeff w = ↑m + ↑n * Complex.I

The coefficients of a rounded polynomial are Gaussian integers.

theorem MIPRE.Tsirelson.l1_roundPoly_sub_le {G : Type u_1} (s : NCPoly G) : (roundPoly s - s).l1 ≤ ↑s.coeff.support.card

The rounding error of a polynomial has ℓ¹ norm at most the size of its support.

theorem MIPRE.Tsirelson.l1_mul_mul_le {G : Type u_1} (x y z : NCPoly G) : (x * y * z).l1 ≤ x.l1 * y.l1 * z.l1

The ℓ¹ norm of a product of three factors.

theorem MIPRE.Tsirelson.l1_elim_one_gen {G : Type u_1} (g : Option G) : (g.elim 1 NCPoly.gen).l1 = 1

The unit and the letters have ℓ¹ norm 1.

theorem MIPRE.Tsirelson.l1_single_mul_mul_single_le {G : Type u_1} (w w' : FreeMonoid G) (ρ : NCPoly G) : (NCPoly.single w 1 * ρ * NCPoly.single w' 1).l1 ≤ ρ.l1

A monomial w ρ w' has ℓ¹ norm at most that of ρ.

theorem MIPRE.Tsirelson.l1_sq_smul_sub_roundPoly_le {G : Type u_1} {N : ℕ} (hN : 1 ≤ N) (g : Option G) (s : NCPoly G) : (↑N ^ 2 • (star s * g.elim 1 NCPoly.gen * s) - star (roundPoly (↑N • s)) * g.elim 1 NCPoly.gen * roundPoly (↑N • s)).l1 ≤ ↑N * (2 * ↑s.coeff.support.card * s.l1 + ↑s.coeff.support.card ^ 2)

Rounding a hermitian square at scale N. With K the size of the support of s, the rounding s̃ of N s satisfies ‖N² s⋆ g s - s̃⋆ g s̃‖₁ ≤ N (2 K ‖s‖₁ + K²).

theorem MIPRE.Tsirelson.l1_sq_smul_sub_roundC_le {G : Type u_1} (N : ℕ) (c : ℂ) (w w' : FreeMonoid G) (ρ : NCPoly G) : (↑N ^ 2 • c • (NCPoly.single w 1 * ρ * NCPoly.single w' 1) - roundC (↑N ^ 2 * c) • (NCPoly.single w 1 * ρ * NCPoly.single w' 1)).l1 ≤ ρ.l1

Rounding an ideal monomial at scale N². Rounding the scalar N² c of N² c · w ρ w' costs at most ‖ρ‖₁.

noncomputable def MIPRE.Tsirelson.roundSos {G : Type u_1} (N : ℕ) (σ : List (Option G × NCPoly G)) : List (Option G × NCPoly G)

Rounding a list of hermitian squares at scale N.

Equations

• MIPRE.Tsirelson.roundSos N σ = List.map (fun (p : Option G × MIPRE.NCPoly G) => (p.1, MIPRE.Tsirelson.roundPoly (↑N • p.2))) σ

noncomputable def MIPRE.Tsirelson.roundIdeal {G : Type u_1} {R : Set (NCPoly G)} (N : ℕ) (ι : List (ℂ × FreeMonoid G × { ρ : NCPoly G // ρ ∈ R } × FreeMonoid G)) : List (ℂ × FreeMonoid G × { ρ : NCPoly G // ρ ∈ R } × FreeMonoid G)

Rounding a list of ideal monomials at scale N².

Equations

• MIPRE.Tsirelson.roundIdeal N ι = List.map (fun (t : ℂ × FreeMonoid G × { ρ : MIPRE.NCPoly G // ρ ∈ R } × FreeMonoid G) => (MIPRE.Tsirelson.roundC (↑N ^ 2 * t.1), t.2)) ι

theorem MIPRE.Tsirelson.l1_sq_smul_sosPoly_sub_le {G : Type u_1} {N : ℕ} (hN : 1 ≤ N) (σ : List (Option G × NCPoly G)) : (↑N ^ 2 • sosPoly σ - sosPoly (roundSos N σ)).l1 ≤ ↑N * (List.map (fun (p : Option G × NCPoly G) => 2 * ↑p.2.coeff.support.card * p.2.l1 + ↑p.2.coeff.support.card ^ 2) σ).sum

The error bound for rounding a list of hermitian squares at scale N.

theorem MIPRE.Tsirelson.l1_sq_smul_idealPoly_sub_le {G : Type u_1} {R : Set (NCPoly G)} (N : ℕ) (ι : List (ℂ × FreeMonoid G × { ρ : NCPoly G // ρ ∈ R } × FreeMonoid G)) : (↑N ^ 2 • idealPoly ι - idealPoly (roundIdeal N ι)).l1 ≤ (List.map (fun (t : ℂ × FreeMonoid G × { ρ : NCPoly G // ρ ∈ R } × FreeMonoid G) => (↑t.2.2.1).l1) ι).sum

The error bound for rounding a list of ideal monomials at scale N².

Certificates for the commuting-operator value

theorem MIPRE.Tsirelson.re_inner_eval_ge {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq (FreeMonoid (Gen X Y A B))] (S : CommutingOperatorStrategy X Y A B) (z : NCPoly (Gen X Y A B)) : (z.coeff 1).re - ∑ w ∈ z.coeff.support.erase 1, (|(z.coeff w).re| + |(z.coeff w).im|) ≤ (inner ℂ S.ψ (((NCPoly.eval (stratEval S)) z) S.ψ)).re

Every strategy is bounded below by the dominance margin. For a commuting-operator strategy S and a polynomial z, Re ⟪ψ, π_S(z) ψ⟫ ≥ Re z_1 - Σ_{w ≠ 1} (|Re z_w| + |Im z_w|): every word evaluates to a contraction.

theorem MIPRE.Tsirelson.commutingOperatorValue_lt_of_dominant {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (G : Game X Y A B) {κ r : ℝ} (hκ : 0 < κ) (σ : List (Option (Gen X Y A B) × NCPoly (Gen X Y A B))) {j : NCPoly (Gen X Y A B)} (hj : j ∈ NCPoly.relSpan (rels X Y A B)) (hT : Dominant ((κ * r) • 1 - κ • gamePoly G - sosPoly σ - j + star ((κ * r) • 1 - κ • gamePoly G - sosPoly σ - j))) : commutingOperatorValue G < r

Soundness of dominant certificates. Let κ > 0, σ a list of hermitian squares and j an element of the relation ideal. If the hermitian part T + T⋆ of T = κ r·1 - κ W_G - Σ s⋆ g s - j is dominant, then the commuting-operator value of G is strictly below r. The margin δ of T + T⋆ bounds 2κ (r - value) below for every strategy, uniformly, so the supremum stays below r - δ / (2κ).

theorem MIPRE.Tsirelson.commutingOperatorValue_lt_of_certificate {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (G : Game X Y A B) {κ r : ℝ} (hκ : 0 < κ) {N : ℕ} (hN : 1 ≤ N) (σ : List (Option (Gen X Y A B) × NCPoly (Gen X Y A B))) (ι : List (ℂ × FreeMonoid (Gen X Y A B) × { ρ : NCPoly (Gen X Y A B) // ρ ∈ rels X Y A B } × FreeMonoid (Gen X Y A B))) (hdom : Dominant (↑N ^ 2 • ((κ * r) • 1 - κ • gamePoly G) - sosPoly σ - idealPoly ι + star (↑N ^ 2 • ((κ * r) • 1 - κ • gamePoly G) - sosPoly σ - idealPoly ι))) : commutingOperatorValue G < r

Soundness of exact certificates. If, at a scale N ≥ 1, the hermitian part of T = N² (κ r·1 - κ W_G) - Σ s⋆ g s - Σ c · w ρ w' is dominant, then the commuting-operator value of G is strictly below r. This is commutingOperatorValue_lt_of_dominant at N² κ; the coefficients need not be Gaussian integers.

theorem MIPRE.Tsirelson.exists_certificate_of_lt {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {κ r : ℝ} (hκ : 0 < κ) (hlt : commutingOperatorValue G < r) : ∃ (N : ℕ), 1 ≤ N ∧ ∃ (σ : List (Option (Gen X Y A B) × NCPoly (Gen X Y A B))) (ι : List (ℂ × FreeMonoid (Gen X Y A B) × { ρ : NCPoly (Gen X Y A B) // ρ ∈ rels X Y A B } × FreeMonoid (Gen X Y A B))), (∀ p ∈ σ, ∀ (w : FreeMonoid (Gen X Y A B)), ∃ (m : ℤ) (n : ℤ), p.2.coeff w = ↑m + ↑n * Complex.I) ∧ (∀ t ∈ ι, ∃ (m : ℤ) (n : ℤ), t.1 = ↑m + ↑n * Complex.I) ∧ Dominant (↑N ^ 2 • ((κ * r) • 1 - κ • gamePoly G) - sosPoly σ - idealPoly ι + star (↑N ^ 2 • ((κ * r) • 1 - κ • gamePoly G) - sosPoly σ - idealPoly ι))

Completeness of dominant certificates. If the commuting-operator value of G is strictly below r and κ > 0, then for some scale N ≥ 1 there are hermitian squares σ and ideal monomials ι, all with Gaussian-integer coefficients, such that the hermitian part of T = N² (κ r·1 - κ W_G) - Σ s⋆ g s - Σ c · w ρ w' is dominant.

theorem MIPRE.Tsirelson.exists_certificate_iff {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (G : Game X Y A B) {κ r : ℝ} (hκ : 0 < κ) : commutingOperatorValue G < r ↔ ∃ (N : ℕ), 1 ≤ N ∧ ∃ (σ : List (Option (Gen X Y A B) × NCPoly (Gen X Y A B))) (ι : List (ℂ × FreeMonoid (Gen X Y A B) × { ρ : NCPoly (Gen X Y A B) // ρ ∈ rels X Y A B } × FreeMonoid (Gen X Y A B))), (∀ p ∈ σ, ∀ (w : FreeMonoid (Gen X Y A B)), ∃ (m : ℤ) (n : ℤ), p.2.coeff w = ↑m + ↑n * Complex.I) ∧ (∀ t ∈ ι, ∃ (m : ℤ) (n : ℤ), t.1 = ↑m + ↑n * Complex.I) ∧ Dominant (↑N ^ 2 • ((κ * r) • 1 - κ • gamePoly G) - sosPoly σ - idealPoly ι + star (↑N ^ 2 • ((κ * r) • 1 - κ • gamePoly G) - sosPoly σ - idealPoly ι))

Exact certificates characterize strict upper bounds on the commuting-operator value, for nonempty answer sets and any κ > 0: the value is below r exactly when, at some scale N ≥ 1, hermitian squares and ideal monomials with Gaussian-integer coefficients make the hermitian part of N² (κ r·1 - κ W_G) - Σ s⋆ g s - Σ c · w ρ w' dominant.