The certificate check is primitive recursive

MIPRE.ValueApprox.primrecPred_check: Check g p q r is a primitive recursive predicate of (g, p, q, r). The proof follows the definitions in MIPRE.Foundations.ValueApprox.RawStrategy one by one, with Mathlib's combinators for lists (Primrec.list_map, list_getD, list_range, the bounded quantifiers PrimrecRel.forall_lt, exists_lt, exists_mem_list) and the arithmetic of MIPRE.Foundations.ValueApprox.RawInt.

theorem HaltingGameValue.GameData.primrec_equivTuple : Primrec ⇑equivTuple

theorem HaltingGameValue.GameData.primrec_nX : Primrec nX

theorem HaltingGameValue.GameData.primrec_nA : Primrec nA

theorem HaltingGameValue.GameData.primrec_w : Primrec w

theorem HaltingGameValue.GameData.primrec_acc : Primrec acc

Generic combinators

theorem MIPRE.ValueApprox.primrec_natSum : Primrec List.sum

theorem MIPRE.ValueApprox.primrecPred_forall_lt {α : Type u_1} [Primcodable α] {n : α → ℕ} {p : α → ℕ → Prop} (hn : Primrec n) (hp : PrimrecRel p) : PrimrecPred fun (a : α) => ∀ i < n a, p a i

theorem MIPRE.ValueApprox.primrecPred_exists_lt {α : Type u_1} [Primcodable α] {n : α → ℕ} {p : α → ℕ → Prop} (hn : Primrec n) (hp : PrimrecRel p) : PrimrecPred fun (a : α) => ∃ i < n a, p a i

theorem MIPRE.ValueApprox.primrec_gsum {α : Type u_1} [Primcodable α] {n : α → ℕ} {f : α → ℕ → GInt} (hn : Primrec n) (hf : Primrec₂ f) : Primrec fun (a : α) => gsum (n a) (f a)

theorem MIPRE.ValueApprox.primrec_psum {α : Type u_1} [Primcodable α] {n : α → ℕ} {f : α → ℕ → PInt} (hn : Primrec n) (hf : Primrec₂ f) : Primrec fun (a : α) => psum (n a) (f a)

theorem MIPRE.ValueApprox.primrec_entry : Primrec fun (p : GMat × ℕ × ℕ) => entry p.1 p.2.1 p.2.2

theorem MIPRE.ValueApprox.primrec_vget : Primrec fun (p : List GInt × ℕ) => vget p.1 p.2

The measurement checks

theorem MIPRE.ValueApprox.primrecPred_isHermRaw : PrimrecPred fun (p : GMat × ℕ) => IsHermRaw p.1 p.2

theorem MIPRE.ValueApprox.primrecPred_isIdemRaw : PrimrecPred fun (p : GMat × ℕ × ℕ) => IsIdemRaw p.1 p.2.1 p.2.2

theorem MIPRE.ValueApprox.primrecPred_isSumRaw : PrimrecPred fun (p : List GMat × ℕ × ℕ × ℕ) => IsSumRaw p.1 p.2.1 p.2.2.1 p.2.2.2

theorem MIPRE.ValueApprox.primrecPred_isPVMRaw : PrimrecPred fun (p : List GMat × ℕ × ℕ × ℕ) => IsPVMRaw p.1 p.2.1 p.2.2.1 p.2.2.2

The value

The compositions below are split into one lemma per level of summation, and intermediate facts are stated without type ascriptions where their type is determined: elaborating a deep composition against a large expected type is what exhausts the heartbeat budget, not the mathematics.

@[reducible, inline]

abbrev MIPRE.ValueApprox.QuadCtx : Type

The context of the Born numerator: the two matrices, the two dimensions, the state.

Equations

• MIPRE.ValueApprox.QuadCtx = ((MIPRE.ValueApprox.GMat × MIPRE.ValueApprox.GMat) × (ℕ × ℕ) × List MIPRE.ValueApprox.GInt)

theorem MIPRE.ValueApprox.primrec_quadRawBody : Primrec fun (x : (((QuadCtx × ℕ) × ℕ) × ℕ) × ℕ) => ((vget x.1.1.1.1.2.2 (x.1.1.1.2 * x.1.1.1.1.2.1.2 + x.1.1.2)).conj.mul ((entry x.1.1.1.1.1.1 x.1.1.1.2 x.1.2).mul (entry x.1.1.1.1.1.2 x.1.1.2 x.2))).mul (vget x.1.1.1.1.2.2 (x.1.2 * x.1.1.1.1.2.1.2 + x.2))

The innermost term of quadRaw, at ((((q, i), j), k), l).

theorem MIPRE.ValueApprox.primrec_quadRaw : Primrec fun (q : QuadCtx) => quadRaw q.1.1 q.1.2 q.2.1.1 q.2.1.2 q.2.2

theorem MIPRE.ValueApprox.primrec_normRaw : Primrec fun (p : List GInt × ℕ × ℕ) => normRaw p.1 p.2.1 p.2.2

theorem MIPRE.ValueApprox.primrec_questionWeight : Primrec fun (p : HaltingGameValue.GameData × ℕ × ℕ) => p.1.questionWeight p.2.1 p.2.2

theorem MIPRE.ValueApprox.sum_range_eq_list_sum (n : ℕ) (f : ℕ → ℕ) : ∑ i ∈ Finset.range n, f i = (List.map f (List.range n)).sum

theorem MIPRE.ValueApprox.totalWeight_eq (g : HaltingGameValue.GameData) : g.totalWeight = (List.map (fun (x : ℕ) => (List.map (fun (y : ℕ) => g.questionWeight x y) (List.range (g.nX + 1))).sum) (List.range (g.nX + 1))).sum

theorem MIPRE.ValueApprox.primrec_questionWeight' : Primrec fun (z : (HaltingGameValue.GameData × ℕ) × ℕ) => z.1.1.questionWeight z.1.2 z.2

theorem MIPRE.ValueApprox.primrec_totalWeightInner : Primrec fun (z : HaltingGameValue.GameData × ℕ) => (List.map (fun (y : ℕ) => z.1.questionWeight z.2 y) (List.range (z.1.nX + 1))).sum

theorem MIPRE.ValueApprox.primrec_totalWeight : Primrec HaltingGameValue.GameData.totalWeight

theorem MIPRE.ValueApprox.primrec_wt : Primrec fun (p : HaltingGameValue.GameData × ℕ × ℕ) => wt p.1 p.2.1 p.2.2

theorem MIPRE.ValueApprox.primrec_W : Primrec W

theorem MIPRE.ValueApprox.primrec_Draw : Primrec fun (p : HaltingGameValue.GameData × ℕ × ℕ × ℕ × ℕ) => Draw p.1 p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2

theorem MIPRE.ValueApprox.primrec_matA : Primrec fun (p : RawStrategy × ℕ × ℕ) => p.1.matA p.2.1 p.2.2

theorem MIPRE.ValueApprox.primrec_matB : Primrec fun (p : RawStrategy × ℕ × ℕ) => p.1.matB p.2.1 p.2.2

@[reducible, inline]

abbrev MIPRE.ValueApprox.NumCtx4 : Type

The contexts of the numerator, from the innermost level ((((g, r), x), y), a), b) out.

Equations

• MIPRE.ValueApprox.NumCtx4 = (((((HaltingGameValue.GameData × MIPRE.ValueApprox.RawStrategy) × ℕ) × ℕ) × ℕ) × ℕ)

@[reducible, inline]

abbrev MIPRE.ValueApprox.NumCtx3 : Type

Equations

• MIPRE.ValueApprox.NumCtx3 = ((((HaltingGameValue.GameData × MIPRE.ValueApprox.RawStrategy) × ℕ) × ℕ) × ℕ)

@[reducible, inline]

abbrev MIPRE.ValueApprox.NumCtx2 : Type

Equations

• MIPRE.ValueApprox.NumCtx2 = (((HaltingGameValue.GameData × MIPRE.ValueApprox.RawStrategy) × ℕ) × ℕ)

@[reducible, inline]

abbrev MIPRE.ValueApprox.NumCtx1 : Type

Equations

• MIPRE.ValueApprox.NumCtx1 = ((HaltingGameValue.GameData × MIPRE.ValueApprox.RawStrategy) × ℕ)

theorem MIPRE.ValueApprox.primrec_numerBody : Primrec fun (x : NumCtx4) => if Draw x.1.1.1.1.1 x.1.1.1.2 x.1.1.2 x.1.2 x.2 = true then (quadRaw (x.1.1.1.1.2.matA x.1.1.1.2 x.1.2) (x.1.1.1.1.2.matB x.1.1.2 x.2) x.1.1.1.1.2.dA x.1.1.1.1.2.dB x.1.1.1.1.2.v).1 else PInt.zero

The innermost term of numer.

theorem MIPRE.ValueApprox.primrec_numer3 : Primrec fun (x : NumCtx3) => psum (x.1.1.1.1.nA + 1) fun (b : ℕ) => if Draw x.1.1.1.1 x.1.1.2 x.1.2 x.2 b = true then (quadRaw (x.1.1.1.2.matA x.1.1.2 x.2) (x.1.1.1.2.matB x.1.2 b) x.1.1.1.2.dA x.1.1.1.2.dB x.1.1.1.2.v).1 else PInt.zero

theorem MIPRE.ValueApprox.primrec_numer2sum : Primrec fun (x : NumCtx2) => psum (x.1.1.1.nA + 1) fun (a : ℕ) => psum (x.1.1.1.nA + 1) fun (b : ℕ) => if Draw x.1.1.1 x.1.2 x.2 a b = true then (quadRaw (x.1.1.2.matA x.1.2 a) (x.1.1.2.matB x.2 b) x.1.1.2.dA x.1.1.2.dB x.1.1.2.v).1 else PInt.zero

theorem MIPRE.ValueApprox.primrec_numer2wt : Primrec fun (x : NumCtx2) => PInt.ofNat (wt x.1.1.1 x.1.2 x.2)

theorem MIPRE.ValueApprox.primrec_numer2 : Primrec fun (x : NumCtx2) => (PInt.ofNat (wt x.1.1.1 x.1.2 x.2)).mul (psum (x.1.1.1.nA + 1) fun (a : ℕ) => psum (x.1.1.1.nA + 1) fun (b : ℕ) => if Draw x.1.1.1 x.1.2 x.2 a b = true then (quadRaw (x.1.1.2.matA x.1.2 a) (x.1.1.2.matB x.2 b) x.1.1.2.dA x.1.1.2.dB x.1.1.2.v).1 else PInt.zero)

theorem MIPRE.ValueApprox.primrec_numer1 : Primrec fun (x : NumCtx1) => psum (x.1.1.nX + 1) fun (y : ℕ) => (PInt.ofNat (wt x.1.1 x.2 y)).mul (psum (x.1.1.nA + 1) fun (a : ℕ) => psum (x.1.1.nA + 1) fun (b : ℕ) => if Draw x.1.1 x.2 y a b = true then (quadRaw (x.1.2.matA x.2 a) (x.1.2.matB y b) x.1.2.dA x.1.2.dB x.1.2.v).1 else PInt.zero)

theorem MIPRE.ValueApprox.primrec_numer : Primrec fun (p : HaltingGameValue.GameData × RawStrategy) => numer p.1 p.2

@[reducible, inline]

abbrev MIPRE.ValueApprox.CheckCtx : Type

The context of the check: ((g, p, q), r).

Equations

• MIPRE.ValueApprox.CheckCtx = ((HaltingGameValue.GameData × ℕ × ℕ) × MIPRE.ValueApprox.RawStrategy)

theorem MIPRE.ValueApprox.primrecPred_valueTest : PrimrecPred fun (p : CheckCtx) => ValueTest p.1.1 p.1.2.1 p.1.2.2 p.2

theorem MIPRE.ValueApprox.primrecPred_checkA : PrimrecPred fun (p : CheckCtx) => ∀ x < p.1.1.nX + 1, IsPVMRaw (p.2.QA.getD x []) p.1.1.nA p.2.dA p.2.k

theorem MIPRE.ValueApprox.primrecPred_checkB : PrimrecPred fun (p : CheckCtx) => ∀ y < p.1.1.nX + 1, IsPVMRaw (p.2.QB.getD y []) p.1.1.nA p.2.dB p.2.k

theorem MIPRE.ValueApprox.primrecPred_checkVinner : PrimrecRel fun (z : CheckCtx × ℕ) (j : ℕ) => ¬(vget z.1.2.v (z.2 * z.1.2.dB + j)).Eq' GInt.zero

theorem MIPRE.ValueApprox.primrecPred_checkVmid : PrimrecRel fun (p : CheckCtx) (i : ℕ) => ∃ j < p.2.dB, ¬(vget p.2.v (i * p.2.dB + j)).Eq' GInt.zero

theorem MIPRE.ValueApprox.primrecPred_checkV : PrimrecPred fun (p : CheckCtx) => ∃ i < p.2.dA, ∃ j < p.2.dB, ¬(vget p.2.v (i * p.2.dB + j)).Eq' GInt.zero

theorem MIPRE.ValueApprox.primrecPred_check : PrimrecPred fun (p : CheckCtx) => Check p.1.1 p.1.2.1 p.1.2.2 p.2

The certificate check is primitive recursive.