Exact strategies, and the quantum value from below

The mathematical core of lem:value-lower-approx (MIP* ⊆ RE): the quantum value of a game exceeds a threshold t if and only if some exact strategy with Gaussian-rational entries has value exceeding t (MIPRE.ValueApprox.lt_quantumValue_iff). Exact strategies (MIPRE.ValueApprox.ExactStrategy) are the raw data of a tensor-product strategy with an unnormalized state — dimensions, measurement operators, a state vector — with validity (ExactStrategy.IsValid: projective measurements, nonzero state) a separate predicate, so that the data can be enumerated and validity checked; their value (ExactStrategy.value) is the Born-rule sum divided by ‖u‖², a rational function of the entries. The computability layer enumerates the Gaussian-rational ones.

• Soundness (ExactStrategy.value_le_quantumValue): valid data describes a tensor-product strategy (ExactStrategy.toStrategy, normalizing the state) of the same value.
• Density (exists_exactStrategy_value_gt): every tensor-product strategy is approximated in value by valid Gaussian-rational exact strategies. The measurement operators are approximated by exact Gaussian-rational projective measurements (IsPVM.exists_entriesIn_norm_sub_le) and the state is rounded entrywise; the value is Lipschitz in the data (abs_bornValue_sub_le), with the crude but sufficient constant 4 |A| |B|.

This departs from the paper's proof of statement (S) in cor:mip-re, which enumerates approximate candidates — Gaussian-rational tuples satisfying relaxed POVM constraints — and repairs each into an exact POVM by T ↦ T^{-1/2} conjugation (its Claims "Stability" and "Density", with the explicit slack Δ(d, k)). Rounding at the level of the skew-Hermitian Cayley generator (MIPRE.Foundations.ValueApprox.Dense) makes every candidate exact, so no repair, no slack and no positive-semidefiniteness test are needed; the biconditional is then sharp.

The Born functional and its perturbation

noncomputable def MIPRE.ValueApprox.bornValue {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {dA : Type u_5} {dB : Type u_6} [Fintype dA] [Fintype dB] (G : Game X Y A B) (P : X → A → Matrix dA dA ℂ) (Q : Y → B → Matrix dB dB ℂ) (ψ : dA × dB → ℂ) : ℝ

The value in G of the strategy data (P, Q, ψ) — TensorProductStrategy.value on unbundled data; the state need not be normalized.

Equations

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

theorem MIPRE.TensorProductStrategy.value_eq_bornValue {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) : S.value = ValueApprox.bornValue G S.PA.M S.PB.M S.ψ

theorem MIPRE.ValueApprox.abs_re_dotProduct_kronecker_sub_le {dA : Type u_5} {dB : Type u_6} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (P P' : Matrix dA dA ℂ) (Q Q' : Matrix dB dB ℂ) {ψ ψ' : dA × dB → ℂ} (hψ : ‖WithLp.toLp 2 ψ‖ = 1) (hψ' : ‖WithLp.toLp 2 ψ'‖ = 1) : |(star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P Q).mulVec ψ).re - (star ψ' ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P' Q').mulVec ψ').re| ≤ ‖P - P'‖ * ‖Q‖ + ‖P'‖ * ‖Q - Q'‖ + 2 * (‖P'‖ * ‖Q'‖) * ‖WithLp.toLp 2 (ψ - ψ')‖

The Born term re ⟨ψ, (P ⊗ Q) ψ⟩ is Lipschitz in the operators and in the unit state.

theorem MIPRE.ValueApprox.abs_sum_sub_sum_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (t t' : X → Y → A → B → ℝ) {c : ℝ} (h : ∀ (x : X) (y : Y) (a : A) (b : B), |t x y a b - t' x y a b| ≤ c) : |∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, (G.μ x y * if G.D x y a b = true then 1 else 0) * t x y a b - ∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, (G.μ x y * if G.D x y a b = true then 1 else 0) * t' x y a b| ≤ ↑(Fintype.card A) * ↑(Fintype.card B) * c

A μ-weighted, D-selected difference of Born sums is bounded termwise: if every term moves by at most c, the sum moves by at most |A| |B| c.

theorem MIPRE.ValueApprox.abs_bornValue_sub_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {dA : Type u_5} {dB : Type u_6} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (G : Game X Y A B) {P P' : X → A → Matrix dA dA ℂ} {Q Q' : Y → B → Matrix dB dB ℂ} {ψ ψ' : dA × dB → ℂ} (hP' : ∀ (x : X), IsPVM (P' x)) (hQ : ∀ (y : Y), IsPVM (Q y)) (hQ' : ∀ (y : Y), IsPVM (Q' y)) (hψ : ‖WithLp.toLp 2 ψ‖ = 1) (hψ' : ‖WithLp.toLp 2 ψ'‖ = 1) {η : ℝ} (hPη : ∀ (x : X) (a : A), ‖P x a - P' x a‖ ≤ η) (hQη : ∀ (y : Y) (b : B), ‖Q y b - Q' y b‖ ≤ η) (hψη : ‖WithLp.toLp 2 (ψ - ψ')‖ ≤ η) : |bornValue G P Q ψ - bornValue G P' Q' ψ'| ≤ ↑(Fintype.card A) * ↑(Fintype.card B) * (4 * η)

The value is Lipschitz in the strategy data: if every measurement operator moves by at most η in operator norm and the unit state by at most η, the value moves by at most 4 |A| |B| η.

Exact strategies

structure MIPRE.ValueApprox.ExactStrategy (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) : Type (max (max (max u_5 u_6) u_7) u_8)

The raw data of a tensor-product strategy with an unnormalized state: dimensions, measurement operators, and a state vector. Whether the data describes a strategy is the separate predicate ExactStrategy.IsValid, so that the data can be enumerated and validity checked.

• dA : ℕ

  The dimension of the first player's space.

• dB : ℕ

  The dimension of the second player's space.

• PA : X → A → Matrix (Fin self.dA) (Fin self.dA) ℂ

  The first player's measurement operators.

• PB : Y → B → Matrix (Fin self.dB) (Fin self.dB) ℂ

  The second player's measurement operators.

• u : Fin self.dA × Fin self.dB → ℂ

  The (unnormalized) shared state.

structure MIPRE.ValueApprox.ExactStrategy.IsValid {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] (c : ExactStrategy X Y A B) : Prop

The data describes a strategy: projective measurements and a nonzero state.

• isPVM_A (x : X) : IsPVM (c.PA x)
• isPVM_B (y : Y) : IsPVM (c.PB y)
• u_ne_zero : c.u ≠ 0

def MIPRE.ValueApprox.ExactStrategy.EntriesIn {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (c : ExactStrategy X Y A B) (K : Subfield ℂ) : Prop

All entries of the data lie in the subfield K.

Equations

• c.EntriesIn K = ((∀ (x : X) (a : A), MIPRE.ValueApprox.EntriesIn K (c.PA x a)) ∧ (∀ (y : Y) (b : B), MIPRE.ValueApprox.EntriesIn K (c.PB y b)) ∧ ∀ (i : Fin c.dA × Fin c.dB), c.u i ∈ K)

noncomputable def MIPRE.ValueApprox.ExactStrategy.value {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (c : ExactStrategy X Y A B) (G : Game X Y A B) : ℝ

The value of the data in G: the Born-rule sum for the unnormalized state, divided by ‖u‖². A rational function of the entries.

Equations

• c.value G = MIPRE.ValueApprox.bornValue G c.PA c.PB c.u / (star c.u ⬝ᵥ c.u).re

noncomputable def MIPRE.ValueApprox.ExactStrategy.ψ {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (c : ExactStrategy X Y A B) : Fin c.dA × Fin c.dB → ℂ

The normalized state u / ‖u‖.

Equations

• c.ψ = (↑‖WithLp.toLp 2 c.u‖)⁻¹ • c.u

theorem MIPRE.ValueApprox.ExactStrategy.star_smul_dotProduct_mulVec_smul {n : Type u_5} [Fintype n] (k : ℂ) (T : Matrix n n ℂ) (u : n → ℂ) : star (k • u) ⬝ᵥ T.mulVec (k • u) = star k * k * star u ⬝ᵥ T.mulVec u

theorem MIPRE.ValueApprox.ExactStrategy.star_ofReal_inv_mul_self (r : ℝ) : star (↑r)⁻¹ * (↑r)⁻¹ = ↑(r ^ 2)⁻¹

theorem MIPRE.ValueApprox.ExactStrategy.ψ_unit {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] (c : ExactStrategy X Y A B) (hc : c.IsValid) : star c.ψ ⬝ᵥ c.ψ = 1

theorem MIPRE.ValueApprox.ExactStrategy.norm_toLp_ψ {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] (c : ExactStrategy X Y A B) (hc : c.IsValid) : ‖WithLp.toLp 2 c.ψ‖ = 1

noncomputable def MIPRE.ValueApprox.ExactStrategy.toStrategy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (c : ExactStrategy X Y A B) (G : Game X Y A B) (hc : c.IsValid) : TensorProductStrategy G

The tensor-product strategy described by valid data: normalize the state.

Equations

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

theorem MIPRE.ValueApprox.ExactStrategy.value_toStrategy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (c : ExactStrategy X Y A B) (G : Game X Y A B) (hc : c.IsValid) : (c.toStrategy G hc).value = c.value G

The value of the data is the value of the strategy it describes.

theorem MIPRE.ValueApprox.ExactStrategy.value_eq_bornValue_ψ {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (c : ExactStrategy X Y A B) (G : Game X Y A B) (hc : c.IsValid) : c.value G = bornValue G c.PA c.PB c.ψ

theorem MIPRE.ValueApprox.ExactStrategy.value_le_quantumValue {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (c : ExactStrategy X Y A B) (G : Game X Y A B) (hc : c.IsValid) : c.value G ≤ quantumValue G

Soundness: the value of valid data is at most the quantum value.

Density

theorem MIPRE.ValueApprox.exists_exactStrategy_value_gt {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (S : TensorProductStrategy G) {ε : ℝ} (hε : 0 < ε) : ∃ (c : ExactStrategy X Y A B), c.IsValid ∧ c.EntriesIn GaussianRat ∧ S.value - ε < c.value G

Every tensor-product strategy is approximated, in value, by valid Gaussian-rational exact strategies: round the measurements to exact Gaussian-rational projective measurements and the state entrywise.

The quantum value from below

def MIPRE.ValueApprox.pointMeasurement (X : Type u_5) {A : Type u_6} [Fintype A] [DecidableEq A] (a₀ : A) : ProjectiveMeasurement X A (Matrix (Fin 1) (Fin 1) ℂ)

The projective measurement on ℂ¹ that always answers a₀.

Equations

• MIPRE.ValueApprox.pointMeasurement X a₀ = { M := fun (x : X) (a : A) => if a = a₀ then 1 else 0, selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ }

theorem MIPRE.ValueApprox.nonempty_tensorProductStrategy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (G : Game X Y A B) : Nonempty (TensorProductStrategy G)

A strategy exists as soon as both answer alphabets are nonempty: one-dimensional spaces and the measurements that always answer a₀, b₀.

theorem MIPRE.ValueApprox.lt_quantumValue_iff {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (G : Game X Y A B) (t : ℝ) : t < quantumValue G ↔ ∃ (c : ExactStrategy X Y A B), c.IsValid ∧ c.EntriesIn GaussianRat ∧ t < c.value G

The quantum value from below. val*(G) > t if and only if some valid exact strategy with Gaussian-rational entries has value greater than t. This is the mathematical content of lem:value-lower-approx: the right-hand side is a semi-decidable condition, as the Gaussian-rational data can be enumerated, validity is a finite set of polynomial identities in the entries, and the value is a rational function of them.