The certificate check is correct

MIPRE.ValueApprox.check_iff_interp: Check g p q r holds iff the exact strategy interp r denoted by the raw candidate is valid for the game g.game and has value greater than p / q. Together with the soundness and density of exact strategies (MIPRE.Foundations.ValueApprox.Strategy) this gives exists_check_iff: some raw candidate passes the check iff p / q < val*(G_g) — the semantic content of the semidecision procedure of lem:value-lower-approx.

The proof reads each clause of Check as the corresponding statement about interp r, with k ≠ 0: the Hermitian, idempotence and completeness tests as the projective-measurement axioms of mat M d k = (M i j / k), the state test as u ≠ 0, and the value test as p / q < value, the value being numer / (W · k² · ⟨v, v⟩). The converse direction of exists_check_iff needs a raw candidate denoting a given valid Gaussian-rational exact strategy, which exists_rawStrategy_interp_eq builds from a common denominator of its entries.

Sums

theorem MIPRE.ValueApprox.toC_gsum_fin (n : ℕ) (f : ℕ → GInt) : (gsum n f).toC = ∑ i : Fin n, (f ↑i).toC

theorem MIPRE.ValueApprox.toInt_psum_fin (n : ℕ) (f : ℕ → PInt) : (psum n f).toInt = ∑ i : Fin n, (f ↑i).toInt

Matrices

noncomputable def MIPRE.ValueApprox.mat (M : GMat) (d k : ℕ) : Matrix (Fin d) (Fin d) ℂ

The d × d complex matrix with entries M i j / k.

Equations

• MIPRE.ValueApprox.mat M d k = Matrix.of fun (i j : Fin d) => (MIPRE.ValueApprox.entry M ↑i ↑j).toC / ↑k

theorem MIPRE.ValueApprox.isHermRaw_iff {M : GMat} {d k : ℕ} (hk : k ≠ 0) : IsHermRaw M d ↔ (mat M d k).conjTranspose = mat M d k

theorem MIPRE.ValueApprox.div_sq_eq_div_iff {a e k : ℂ} (hk : k ≠ 0) : a / k ^ 2 = e / k ↔ a = k * e

a / k² = e / k ↔ a = k e for k ≠ 0.

theorem MIPRE.ValueApprox.mat_mul_mat_apply {M : GMat} {d k : ℕ} (i j : Fin d) : (mat M d k * mat M d k) i j = (∑ l : Fin d, (entry M ↑i ↑l).toC * (entry M ↑l ↑j).toC) / ↑k ^ 2

theorem MIPRE.ValueApprox.isIdemRaw_iff {M : GMat} {d k : ℕ} (hk : k ≠ 0) : IsIdemRaw M d k ↔ mat M d k * mat M d k = mat M d k

theorem MIPRE.ValueApprox.isSumRaw_iff {d k : ℕ} {Ms : List GMat} {nA : ℕ} (hk : k ≠ 0) : IsSumRaw Ms nA d k ↔ ∑ a : Fin (nA + 1), mat (Ms.getD ↑a []) d k = 1

theorem MIPRE.ValueApprox.isPVMRaw_iff {d k : ℕ} {Ms : List GMat} {nA : ℕ} (hk : k ≠ 0) : IsPVMRaw Ms nA d k ↔ IsPVM fun (a : Fin (nA + 1)) => mat (Ms.getD ↑a []) d k

The state and the Born terms

noncomputable def MIPRE.ValueApprox.vec (dA dB : ℕ) (v : List GInt) (k : ℕ) : Fin dA × Fin dB → ℂ

The state denoted by v, (i, j) ↦ v (i * dB + j) / k.

Equations

• MIPRE.ValueApprox.vec dA dB v k p = (MIPRE.ValueApprox.vget v (↑p.1 * dB + ↑p.2)).toC / ↑k

theorem MIPRE.ValueApprox.vec_ne_zero_iff {k : ℕ} (dA dB : ℕ) (v : List GInt) (hk : k ≠ 0) : vec dA dB v k ≠ 0 ↔ ∃ i < dA, ∃ j < dB, ¬(vget v (i * dB + j)).Eq' GInt.zero

theorem MIPRE.ValueApprox.dotProduct_vec_self {k : ℕ} (dA dB : ℕ) (v : List GInt) (hk : k ≠ 0) : star (vec dA dB v k) ⬝ᵥ vec dA dB v k = (gsum dA fun (i : ℕ) => gsum dB fun (j : ℕ) => (vget v (i * dB + j)).conj.mul (vget v (i * dB + j))).toC / ↑k ^ 2

theorem MIPRE.ValueApprox.re_dotProduct_vec_self {k : ℕ} (dA dB : ℕ) (v : List GInt) (hk : k ≠ 0) : (star (vec dA dB v k) ⬝ᵥ vec dA dB v k).re = ↑(normRaw v dA dB).toInt / ↑k ^ 2

theorem MIPRE.ValueApprox.dotProduct_kronecker_vec {k : ℕ} (dA dB : ℕ) (v : List GInt) (A B : GMat) (hk : k ≠ 0) : star (vec dA dB v k) ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (mat A dA k) (mat B dB k)).mulVec (vec dA dB v k) = (quadRaw A B dA dB v).toC / ↑k ^ 4

theorem MIPRE.ValueApprox.re_dotProduct_kronecker_vec {k : ℕ} (dA dB : ℕ) (v : List GInt) (A B : GMat) (hk : k ≠ 0) : (star (vec dA dB v k) ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (mat A dA k) (mat B dB k)).mulVec (vec dA dB v k)).re = ↑(quadRaw A B dA dB v).1.toInt / ↑k ^ 4

The interpretation

The game

theorem HaltingGameValue.GameData.one_le_W (g : GameData) : 1 ≤ MIPRE.ValueApprox.W g

theorem HaltingGameValue.GameData.game_μ_eq (g : GameData) (x y : Fin (g.nX + 1)) : g.game.μ x y = ↑(MIPRE.ValueApprox.wt g ↑x ↑y) / ↑(MIPRE.ValueApprox.W g)

theorem HaltingGameValue.GameData.game_D_eq (g : GameData) (x y : Fin (g.nX + 1)) (a b : Fin (g.nA + 1)) : g.game.D x y a b = MIPRE.ValueApprox.Draw g ↑x ↑y ↑a ↑b

The value

theorem MIPRE.ValueApprox.toInt_numer (g : HaltingGameValue.GameData) (r : RawStrategy) : ↑(numer g r).toInt = ∑ x : Fin (g.nX + 1), ∑ y : Fin (g.nX + 1), ↑(wt g ↑x ↑y) * ∑ a : Fin (g.nA + 1), ∑ b : Fin (g.nA + 1), if Draw g ↑x ↑y ↑a ↑b = true then ↑(quadRaw (r.matA ↑x ↑a) (r.matB ↑y ↑b) r.dA r.dB r.v).1.toInt else 0

theorem MIPRE.ValueApprox.interp_bornValue (g : HaltingGameValue.GameData) (r : RawStrategy) (hk : r.k ≠ 0) : bornValue g.game (fun (x : Fin (g.nX + 1)) (a : Fin (g.nA + 1)) => mat (r.matA ↑x ↑a) r.dA r.k) (fun (y : Fin (g.nX + 1)) (b : Fin (g.nA + 1)) => mat (r.matB ↑y ↑b) r.dB r.k) (vec r.dA r.dB r.v r.k) = ↑(numer g r).toInt / (↑(W g) * ↑r.k ^ 4)

theorem MIPRE.ValueApprox.interp_value (g : HaltingGameValue.GameData) (r : RawStrategy) (hk : r.k ≠ 0) : (RawStrategy.interp g.nX g.nA r).value g.game = ↑(numer g r).toInt / (↑(W g) * ↑r.k ^ 2 * ↑(normRaw r.v r.dA r.dB).toInt)

theorem MIPRE.ValueApprox.normRaw_pos {dA dB : ℕ} {v : List GInt} {k : ℕ} (hk : k ≠ 0) (hv : vec dA dB v k ≠ 0) : 0 < (normRaw v dA dB).toInt

theorem MIPRE.ValueApprox.valueTest_iff (g : HaltingGameValue.GameData) (p q : ℕ) (r : RawStrategy) (hk : r.k ≠ 0) (hv : vec r.dA r.dB r.v r.k ≠ 0) : ValueTest g p q r ↔ ↑p / ↑q < (RawStrategy.interp g.nX g.nA r).value g.game

The check is correct

theorem MIPRE.ValueApprox.check_iff_interp (g : HaltingGameValue.GameData) (p q : ℕ) (r : RawStrategy) : Check g p q r ↔ (RawStrategy.interp g.nX g.nA r).IsValid ∧ ↑p / ↑q < (RawStrategy.interp g.nX g.nA r).value g.game