Raw candidates and the certificate check

The enumeration behind lem:value-lower-approx ranges over raw candidates (MIPRE.ValueApprox.RawStrategy): a common denominator k, two dimensions, the Gaussian-integer numerators of the measurement operators as lists of list matrices, and the numerators of the state. A raw candidate denotes an exact strategy (RawStrategy.interp), with entries in (1/k) ℤ[i]; the predicate Check g p q r says, in exact integer arithmetic, that the candidate is a valid strategy for the game described by g and that its value exceeds p / q:

• IsPVMRaw: each family of operators is Hermitian, idempotent (M² = k M) and sums to k·1;
• the state is nonzero;
• ValueTest: p · W · k² · ⟨v, v⟩ < q · numer, where numer is ∑ wt(x,y) ∑ D re ⟨v, (A ⊗ B) v⟩ and W the total weight (the point mass on (0,0) when the weights vanish, as in GameData.toGame); for q = 0, where p / q = 0, the test is 0 < numer.

All of it is primitive recursive (MIPRE.Foundations.ValueApprox.RawPrimrec), and MIPRE.Foundations.ValueApprox.RawSemantics proves that Check g p q r holds iff interp r is valid with value above p / q.

Matrices and vectors as lists

@[reducible, inline]

abbrev MIPRE.ValueApprox.GMat : Type

A matrix as a list of rows; missing entries read as 0.

Equations

• MIPRE.ValueApprox.GMat = List (List MIPRE.ValueApprox.GInt)

def MIPRE.ValueApprox.entry (M : GMat) (i j : ℕ) : GInt

The (i, j) entry of a list matrix, 0 when missing.

Equations

• MIPRE.ValueApprox.entry M i j = (List.getD M i []).getD j MIPRE.ValueApprox.GInt.zero

def MIPRE.ValueApprox.vget (v : List GInt) (i : ℕ) : GInt

The i-th entry of a list vector, 0 when missing.

Equations

• MIPRE.ValueApprox.vget v i = v.getD i MIPRE.ValueApprox.GInt.zero

def MIPRE.ValueApprox.gsum (n : ℕ) (f : ℕ → GInt) : GInt

∑_{l < n} f l in GInt.

Equations

• MIPRE.ValueApprox.gsum n f = MIPRE.ValueApprox.GInt.sum (List.map f (List.range n))

def MIPRE.ValueApprox.psum (n : ℕ) (f : ℕ → PInt) : PInt

∑_{l < n} f l in PInt.

Equations

• MIPRE.ValueApprox.psum n f = MIPRE.ValueApprox.PInt.sum (List.map f (List.range n))

theorem MIPRE.ValueApprox.toC_gsum (n : ℕ) (f : ℕ → GInt) : (gsum n f).toC = ∑ i ∈ Finset.range n, (f i).toC

theorem MIPRE.ValueApprox.toInt_psum (n : ℕ) (f : ℕ → PInt) : (psum n f).toInt = ∑ i ∈ Finset.range n, (f i).toInt

Raw candidates

structure MIPRE.ValueApprox.RawStrategy : Type

The raw data of a candidate: a common denominator k, the two dimensions, the numerators of the first and second players' operators (indexed by question, then answer), and the numerators of the state, in row-major order (i, j) ↦ i * dB + j.

• k : ℕ
• dA : ℕ
• dB : ℕ
• QA : List (List GMat)
• QB : List (List GMat)
• v : List GInt

def MIPRE.ValueApprox.RawStrategy.equivTuple : RawStrategy ≃ ℕ × ℕ × ℕ × List (List GMat) × List (List GMat) × List GInt

Raw candidates are tuples.

Equations

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

@[instance_reducible]

instance MIPRE.ValueApprox.RawStrategy.instPrimcodable : Primcodable RawStrategy

Equations

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

theorem MIPRE.ValueApprox.RawStrategy.primrec_equivTuple : Primrec ⇑equivTuple

theorem MIPRE.ValueApprox.RawStrategy.primrec_k : Primrec k

theorem MIPRE.ValueApprox.RawStrategy.primrec_dA : Primrec dA

theorem MIPRE.ValueApprox.RawStrategy.primrec_dB : Primrec dB

theorem MIPRE.ValueApprox.RawStrategy.primrec_QA : Primrec QA

theorem MIPRE.ValueApprox.RawStrategy.primrec_QB : Primrec QB

theorem MIPRE.ValueApprox.RawStrategy.primrec_v : Primrec v

def MIPRE.ValueApprox.RawStrategy.matA (r : RawStrategy) (x a : ℕ) : GMat

The numerator matrix of the first player's operator for question x and answer a.

Equations

• r.matA x a = (r.QA.getD x []).getD a []

def MIPRE.ValueApprox.RawStrategy.matB (r : RawStrategy) (y b : ℕ) : GMat

The numerator matrix of the second player's operator for question y and answer b.

Equations

• r.matB y b = (r.QB.getD y []).getD b []

noncomputable def MIPRE.ValueApprox.RawStrategy.interp (nX nA : ℕ) (r : RawStrategy) : ExactStrategy (Fin (nX + 1)) (Fin (nX + 1)) (Fin (nA + 1)) (Fin (nA + 1))

The exact strategy denoted by raw data, for question alphabet Fin (nX + 1) and answer alphabet Fin (nA + 1): every numerator divided by k.

Equations

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

The certificate check

def MIPRE.ValueApprox.IsHermRaw (M : GMat) (d : ℕ) : Prop

The d × d matrix M is Hermitian.

Equations

• MIPRE.ValueApprox.IsHermRaw M d = ∀ i < d, ∀ j < d, (MIPRE.ValueApprox.entry M i j).Eq' (MIPRE.ValueApprox.entry M j i).conj

def MIPRE.ValueApprox.IsIdemRaw (M : GMat) (d k : ℕ) : Prop

M² = k M, i.e. M / k is idempotent.

Equations

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

def MIPRE.ValueApprox.IsSumRaw (Ms : List GMat) (nA d k : ℕ) : Prop

∑_{a ≤ nA} Mₐ = k · 1.

Equations

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

def MIPRE.ValueApprox.IsPVMRaw (Ms : List GMat) (nA d k : ℕ) : Prop

(Mₐ / k)_{a ≤ nA} is a projective measurement on ℂ^d.

Equations

• MIPRE.ValueApprox.IsPVMRaw Ms nA d k = ((∀ a < nA + 1, MIPRE.ValueApprox.IsHermRaw (Ms.getD a []) d ∧ MIPRE.ValueApprox.IsIdemRaw (Ms.getD a []) d k) ∧ MIPRE.ValueApprox.IsSumRaw Ms nA d k)

def MIPRE.ValueApprox.quadRaw (A B : GMat) (dA dB : ℕ) (v : List GInt) : GInt

The Born numerator ⟨v, (A ⊗ B) v⟩ for v of length dA * dB in row-major order.

Equations

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

def MIPRE.ValueApprox.normRaw (v : List GInt) (dA dB : ℕ) : PInt

The real part of ⟨v, v⟩ for v of length dA * dB in row-major order.

Equations

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

def MIPRE.ValueApprox.wt (g : HaltingGameValue.GameData) (x y : ℕ) : ℕ

The unnormalized question weight of the description on (x, y), with the point mass on (0, 0) when the total weight vanishes, as in GameData.toGame.

Equations

• MIPRE.ValueApprox.wt g x y = if g.totalWeight = 0 then if x = 0 ∧ y = 0 then 1 else 0 else g.questionWeight x y

def MIPRE.ValueApprox.W (g : HaltingGameValue.GameData) : ℕ

The normalizing weight: 1 when the total weight vanishes.

Equations

• MIPRE.ValueApprox.W g = if g.totalWeight = 0 then 1 else g.totalWeight

def MIPRE.ValueApprox.Draw (g : HaltingGameValue.GameData) (x y a b : ℕ) : Bool

The decision predicate of the description, on naturals.

Equations

• MIPRE.ValueApprox.Draw g x y a b = if x = y ∧ a ≠ b then false else decide ((x, y, a, b) ∈ g.acc)

def MIPRE.ValueApprox.numer (g : HaltingGameValue.GameData) (r : RawStrategy) : PInt

∑_{x, y} wt(x, y) ∑_{a, b} D(x, y, a, b) · re ⟨v, (A^x_a ⊗ B^y_b) v⟩.

Equations

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

def MIPRE.ValueApprox.ValueTest (g : HaltingGameValue.GameData) (p q : ℕ) (r : RawStrategy) : Prop

p / q < value, cleared of denominators: p · W · k² · ⟨v, v⟩ < q · numer; for q = 0, where p / q = 0, the test is 0 < numer.

Equations

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

def MIPRE.ValueApprox.Check (g : HaltingGameValue.GameData) (p q : ℕ) (r : RawStrategy) : Prop

The candidate r certifies p / q < val*(G_g): positive denominator, projective measurements on both sides, a nonzero state, and the value test.

Equations

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

@[instance_reducible]

instance MIPRE.ValueApprox.instDecidableIsHermRaw (M : GMat) (d : ℕ) : Decidable (IsHermRaw M d)

Equations

• MIPRE.ValueApprox.instDecidableIsHermRaw M d = id inferInstance

@[instance_reducible]

instance MIPRE.ValueApprox.instDecidableIsIdemRaw (M : GMat) (d k : ℕ) : Decidable (IsIdemRaw M d k)

Equations

• MIPRE.ValueApprox.instDecidableIsIdemRaw M d k = id inferInstance

@[instance_reducible]

instance MIPRE.ValueApprox.instDecidableIsSumRaw (Ms : List GMat) (nA d k : ℕ) : Decidable (IsSumRaw Ms nA d k)

Equations

• MIPRE.ValueApprox.instDecidableIsSumRaw Ms nA d k = id inferInstance

@[instance_reducible]

instance MIPRE.ValueApprox.instDecidableIsPVMRaw (Ms : List GMat) (nA d k : ℕ) : Decidable (IsPVMRaw Ms nA d k)

Equations

• MIPRE.ValueApprox.instDecidableIsPVMRaw Ms nA d k = id inferInstance

@[instance_reducible]

instance MIPRE.ValueApprox.instDecidableValueTest (g : HaltingGameValue.GameData) (p q : ℕ) (r : RawStrategy) : Decidable (ValueTest g p q r)

Equations

• MIPRE.ValueApprox.instDecidableValueTest g p q r = id inferInstance

@[instance_reducible]

instance MIPRE.ValueApprox.instDecidableCheck (g : HaltingGameValue.GameData) (p q : ℕ) (r : RawStrategy) : Decidable (Check g p q r)

Equations

• MIPRE.ValueApprox.instDecidableCheck g p q r = id inferInstance