Deciding acceptance under a time bound

The first half of obligation O2 (blueprint rem:compression-abstract, item 3): the acceptance table of the tabulated game. Filling it in needs Decider.Accepts — a Σ₁ statement, ∃ t, prog.Runs … — to be decided, and that is exactly what n-boundedness buys: the bound supplies a budget within which the decider must halt, so one budgeted run settles the question (Machine.runForD).

• Decider.acceptBudget: the budget T · (|d| + 1) ^ k the bound gives at index n on the tuple (x, y, a, b), read off the shape of Decider.TimeBoundAt.
• Decider.accepts_iff_runForD: for a decider obeying that bound, acceptance is one budgeted run returning encode true.
• Decider.decidableAccepts and Verifier.decidableAccepts: the resulting decision procedures, and Verifier.accepts_iff_runForD for the verifier a string denotes, where the bound comes from Verifier.IsBounded.

The other half of the tabulation is the question distribution, and the rest of this file is what a GameData needs for it. CL.Sampler.queryUnder runs one sampler query under the same kind of budget; Verifier.bitsToIdx turns the bit string a query returns into the number a GameData names its questions by, and agrees with Verifier.questionEquiv; and Verifier.weightList is the weight list itself — one entry of weight 1 for each point of 𝔽₂^{s(n)}, at the index pair its two marginals land on. Its questionWeight is then the number of points landing on a given pair and its totalWeight is 2 ^ s(n), which is exactly the quotient CL.clDist is: length_filter_bitStrsOfLen is the bridge, the bit strings of length s being the vectors of 𝔽₂^s.

Verifier.answerEquiv_symm_val is the same service on the answer side: an answer's index is its position among the bit strings of length at most T, the enumeration answerList being bitStrsLE mapped by a truncation that is the identity on them.

Verifier.accListW is then the acceptance table: the index tuples of the answer tuples a predicate accepts, enumerated over the two alphabets, with mem_accListW_iff saying exactly what is in it. It takes the two question indexings fA, fB as parameters, because the tabulation tags Alice's question differently from Bob's; Verifier.accList is the case fA = fB = bitsToIdx and is the same list definitionally, so nothing downstream of the old name changed. bitsToIdx_injOn is what lets a tuple be read back — the index of a question determines it, among the strings of a fixed length — and tagEquiv is the tagged alphabet it supports: a tag bit and a point of 𝔽₂^s packed into one index by prepending the tag, so that bitsToIdx_lt and bitsToIdx_injOn apply verbatim at s + 1.

MIPRE.Halting.tabOf at the end assembles all of it: the GameData two encoded programs and five numbers describe, with primrec_tabOf its computability. Plain data and not a verifier, because a Verifier is a structure carrying proofs and so is not the sort of thing a Primrec statement can mention; the bridge back to the verifier those parameters came from is in Halting/Instantiation.lean.

Nothing here is efficient and nothing needs to be: the tabulation is a computable map, not a polynomial-time one. The budget is not one number: the two sampler runs take theirs as the parameters B, k, so that a caller can pass the sampler's own time bound, while accOf alone runs at the n ^ n that the verifier's n-boundedness supplies.

def MIPRE.Decider.acceptBudget (T k : ℕ) (x y a b : Cost.BitStr) : ℕ

The budget the time bound TimeBoundAt n T k gives on the tuple (x, y, a, b): the decider's input is cons (encode n) (encode (x, y, a, b)), and the bound is T times the k-th power of one more than the size of the second component.

Equations

• MIPRE.Decider.acceptBudget T k x y a b = T * ((MIPRE.Cost.encode (x, y, a, b)).size + 1) ^ k

theorem MIPRE.Decider.accepts_iff_runForD (D : Decider) {n T k : ℕ} (hb : D.TimeBoundAt n T k) (x y a b : Cost.BitStr) : D.Accepts n x y a b ↔ Cost.Machine.runForD (Cost.encode D.prog) (Cost.encode (n, x, y, a, b)) (acceptBudget T k x y a b) = some (Cost.encode true)

Acceptance under a time bound is one budgeted run.

def MIPRE.Decider.decidableAccepts (D : Decider) {n T k : ℕ} (hb : D.TimeBoundAt n T k) (x y a b : Cost.BitStr) : Decidable (D.Accepts n x y a b)

Hence acceptance is decidable, for a decider that obeys a time bound at the index.

Equations

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

theorem MIPRE.Verifier.accepts_iff_runForD {ℓ : ℕ} (V : Verifier ℓ) {n : ℕ} (hb : V.IsBounded n) (hn : 2 ≤ n) (x y a b : Cost.BitStr) : V.decider.Accepts n x y a b ↔ Cost.Machine.runForD (Cost.encode V.decider.prog) (Cost.encode (n, x, y, a, b)) (Decider.acceptBudget (n ^ n) n x y a b) = some (Cost.encode true)

Acceptance by an n-bounded verifier is one budgeted run, at the budget its own λ-boundedness supplies. This is what fills in the acceptance table of the tabulation.

def MIPRE.Verifier.decidableAccepts {ℓ : ℕ} (V : Verifier ℓ) {n : ℕ} (hb : V.IsBounded n) (hn : 2 ≤ n) (x y a b : Cost.BitStr) : Decidable (V.decider.Accepts n x y a b)

Hence acceptance by an n-bounded verifier is decidable.

Equations

• V.decidableAccepts hb hn x y a b = V.decider.decidableAccepts ⋯ x y a b

Sampler queries under the budget

def MIPRE.CL.Sampler.queryUnder {ℓ : ℕ} (S : Sampler ℓ) (T k n : ℕ) (q : Query) : Option Cost.Data

One query to the sampler, run under the budget its time bound supplies. The sampler is required to halt on every input of the form (n, …), so this is total wherever the bound holds.

Equations

• S.queryUnder T k n q = MIPRE.Cost.Machine.runForD (MIPRE.Cost.encode S.prog) (MIPRE.Cost.encode (n, q)) (T * ((MIPRE.Cost.encode q).size + 1) ^ k)

theorem MIPRE.CL.Sampler.queryUnder_eq {ℓ : ℕ} (S : Sampler ℓ) {n T k : ℕ} (hb : S.TimeBoundAt n T k) {q : Query} {r : Cost.Data} {t : ℕ} (h : S.prog.Runs (Cost.encode (n, q)) r t) : S.queryUnder T k n q = some r

Under the bound, a budgeted query returns exactly what the sampler's correctness clauses say it returns.

theorem MIPRE.CL.Sampler.queryUnder_dimension {ℓ : ℕ} (S : Sampler ℓ) {n T k : ℕ} (hb : S.TimeBoundAt n T k) : S.queryUnder T k n Query.dimension = some (Cost.encode (S.dim n))

The dimension query.

theorem MIPRE.CL.Sampler.queryUnder_marginal {ℓ : ℕ} (S : Sampler ℓ) {n T k : ℕ} (hb : S.TimeBoundAt n T k) (hl : 1 ≤ ℓ) (w : Player) (z : Cost.BitStr) (hz : List.length z = S.dim n) : S.queryUnder T k n (Query.marginal w ℓ z) = some (Cost.encode (toBits ((S.cl n w).eval (ofBits (S.dim n) z))))

The marginal at the top level is the CL function itself (CLFun.truncate_self), so one budgeted marginal query at level ℓ computes L^w(z) — which is what the question weights of the tabulated game are counted from.

theorem MIPRE.CL.Sampler.primrec_encode_marginal (w : Player) (j : ℕ) : Primrec fun (z : Cost.BitStr) => Cost.encode (Query.marginal w j z)

A marginal query with the player and the level fixed is a primitive recursive function of the point queried: a query is its tuple, encoded, and marginal w j z is (1, w, j, z, []), so with w and j literal only encode z varies.

Questions as numbers

def MIPRE.Verifier.bitsToIdx : Cost.BitStr → ℕ

The index of a bit string: the number whose binary digits it is, least significant first. This is the ℕ-level form of Verifier.questionEquiv, and it is what the tabulation can actually compute with — the question alphabet of a GameData is Fin (nX + 1), so every question reached by a sampler query has to be turned into a number.

Equations

• MIPRE.Verifier.bitsToIdx [] = 0
• MIPRE.Verifier.bitsToIdx (b :: l) = (if b = true then 1 else 0) + 2 * MIPRE.Verifier.bitsToIdx l

@[simp]

theorem MIPRE.Verifier.bitsToIdx_nil : bitsToIdx [] = 0

@[simp]

theorem MIPRE.Verifier.bitsToIdx_cons (b : Bool) (l : Cost.BitStr) : bitsToIdx (b :: l) = (if b = true then 1 else 0) + 2 * bitsToIdx l

theorem MIPRE.Verifier.bitsToIdx_ofFn {s : ℕ} (f : Fin s → Bool) : bitsToIdx (List.ofFn f) = ∑ i : Fin s, (if f i = true then 1 else 0) * 2 ^ ↑i

theorem MIPRE.Verifier.bitsToIdx_ofFn_fin2 {s : ℕ} (w : Fin s → Fin 2) : bitsToIdx (List.ofFn fun (i : Fin s) => decide (w i = 1)) = ↑(finFunctionFinEquiv w)

The Fin 2 form, where finFunctionFinEquiv is literally applicable: CL.𝔽₂ is ZMod 2, which reduces to Fin 2 but does not unify with it at the transparency rw uses.

@[simp]

theorem MIPRE.Verifier.questionEquiv_symm_val {s : ℕ} (v : Fin s → CL.𝔽₂) : ↑((questionEquiv s).symm v) = bitsToIdx (CL.toBits v)

The index of a question is the number its bit string denotes. This is what lets the tabulation name questions by numbers while the value agreement is read along questionEquiv.

@[simp]

theorem MIPRE.Verifier.bitsToIdx_toBits_questionEquiv {s : ℕ} (i : Fin (2 ^ s)) : bitsToIdx (CL.toBits ((questionEquiv s) i)) = ↑i

The question weights

theorem MIPRE.Verifier.bitsToIdx_lt (l : Cost.BitStr) : bitsToIdx l < 2 ^ List.length l

The index of a bit string is below 2 ^ its length.

theorem MIPRE.Verifier.primrec_bitsToIdx : Primrec bitsToIdx

def MIPRE.Verifier.weightList (s : ℕ) (fA fB : Cost.BitStr → ℕ) : List (ℕ × ℕ × ℕ)

The weight list of a tabulation: one entry of weight 1 for each point of 𝔽₂^s, at the index pair its two marginals land on.

Equations

• MIPRE.Verifier.weightList s fA fB = List.map (fun (z : MIPRE.Cost.BitStr) => (fA z, fB z, 1)) (MIPRE.Cost.Data.bitStrsOfLen s)

theorem MIPRE.Verifier.questionWeight_weightList (nX nA s : ℕ) (fA fB : Cost.BitStr → ℕ) (acc : List (ℕ × ℕ × ℕ × ℕ)) (i j : ℕ) : { nX := nX, nA := nA, w := weightList s fA fB, acc := acc }.questionWeight i j = (List.filter (fun (z : Cost.BitStr) => decide (fA z = i ∧ fB z = j)) (Cost.Data.bitStrsOfLen s)).length

theorem MIPRE.Verifier.sum_filter_length {N : ℕ} (fA fB : Cost.BitStr → ℕ) (l : List Cost.BitStr) (hA : ∀ z ∈ l, fA z < N) (hB : ∀ z ∈ l, fB z < N) : ∑ x : Fin N, ∑ y : Fin N, (List.filter (fun (z : Cost.BitStr) => decide (fA z = ↑x ∧ fB z = ↑y)) l).length = l.length

Every point of 𝔽₂^s is counted once, so the total weight is 2 ^ s.

theorem MIPRE.Verifier.totalWeight_weightList (nX nA s : ℕ) (fA fB : Cost.BitStr → ℕ) (acc : List (ℕ × ℕ × ℕ × ℕ)) (hA : ∀ z ∈ Cost.Data.bitStrsOfLen s, fA z < nX + 1) (hB : ∀ z ∈ Cost.Data.bitStrsOfLen s, fB z < nX + 1) : { nX := nX, nA := nA, w := weightList s fA fB, acc := acc }.totalWeight = 2 ^ s

The total weight of the list is 2 ^ s: every point of 𝔽₂^s contributes 1, and the index pairs it can land on are all in range. That denominator is exactly the one CL.clDist divides by.

theorem MIPRE.Verifier.length_filter_bitStrsOfLen {s : ℕ} (P : (Fin s → CL.𝔽₂) → Bool) : (List.filter (fun (z : Cost.BitStr) => P (CL.ofBits s z)) (Cost.Data.bitStrsOfLen s)).length = {v : Fin s → CL.𝔽₂ | P v = true}.card

Counting over 𝔽₂^s by enumerating bit strings. The bit strings of length s are the vectors of 𝔽₂^s, so a count over one is a count over the other — which is what turns the tabulation's weight list into the numerator of CL.clDist.

Answers as numbers

theorem MIPRE.Verifier.idxOf_map_of_injOn {α : Type u_1} {β : Type u_2} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] (f : α → β) (l : List α) (hinj : ∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y) {x : α} (hx : x ∈ l) : List.idxOf (f x) (List.map f l) = List.idxOf x l

The index of a mapped element, when the map is injective on the list.

theorem MIPRE.Verifier.answerEquiv_symm_val (T : ℕ) (a : Answers T) : ↑((answerEquiv T).symm a) = List.idxOf (↑a) (Cost.Data.bitStrsLE T)

The answers of length at most T are indexed by their position among the bit strings of length at most T: the enumeration answerList is bitStrsLE mapped by truncation, which is the identity on those strings.

The acceptance table

theorem MIPRE.Verifier.bitsToIdx_injOn {s : ℕ} {x y : Cost.BitStr} (hx : List.length x = s) (hy : List.length y = s) (h : bitsToIdx x = bitsToIdx y) : x = y

bitsToIdx is injective on the bit strings of a fixed length: it is the binary expansion, read through questionEquiv.

The doubled question alphabet, indexed

A question of the doubled game is a tag bit and a point of 𝔽₂^s. It is packed into one number by prepending the tag bit to the point's bit string: the index of (b, v) is bitsToIdx (b :: CL.toBits v). Three things this packing buys, and they are the reason for it:

• the packed index is bitsToIdx of a bit string of length s + 1, so bitsToIdx_lt bounds it by 2 ^ (s + 1) and bitsToIdx_injOn — injectivity on strings of a fixed length — reads it back, both verbatim at s + 1;
• Alice's indices are even and Bob's odd, so the two copies are automatically disjoint;
• nothing else in the tabulation changes: the weight list still enumerates 𝔽₂^s.

theorem MIPRE.Verifier.toBits_injective (s : ℕ) : Function.Injective CL.toBits

CL.toBits is injective: it is the binary expansion read by questionEquiv.

theorem MIPRE.Verifier.bitsToIdx_cons_toBits_inj {s : ℕ} {b c : Bool} {v w : Fin s → CL.𝔽₂} (h : bitsToIdx (b :: CL.toBits v) = bitsToIdx (c :: CL.toBits w)) : b = c ∧ v = w

The packing is injective, componentwise. This is bitsToIdx_injOn at length s + 1, which is why the tag is prepended rather than appended or added as an offset.

theorem MIPRE.Verifier.bitsToIdx_cons_toBits_eq_iff {s : ℕ} (b c : Bool) (v w : Fin s → CL.𝔽₂) : bitsToIdx (b :: CL.toBits v) = bitsToIdx (c :: CL.toBits w) ↔ b = c ∧ v = w

def MIPRE.Verifier.tagIdx {s : ℕ} (p : Bool × (Fin s → CL.𝔽₂)) : Fin (2 ^ (s + 1))

The packed index of a tagged question.

Equations

• MIPRE.Verifier.tagIdx p = ⟨MIPRE.Verifier.bitsToIdx (p.1 :: MIPRE.CL.toBits p.2), ⋯⟩

theorem MIPRE.Verifier.tagIdx_injective (s : ℕ) : Function.Injective tagIdx

noncomputable def MIPRE.Verifier.tagEquiv (s : ℕ) : Bool × (Fin s → CL.𝔽₂) ≃ Fin (2 ^ (s + 1))

The doubled question alphabet.

Equations

• MIPRE.Verifier.tagEquiv s = Equiv.ofBijective MIPRE.Verifier.tagIdx ⋯

theorem MIPRE.Verifier.bitsToIdx_tagEquiv_symm (s : ℕ) (i : Fin (2 ^ (s + 1))) : bitsToIdx (((tagEquiv s).symm i).1 :: CL.toBits ((tagEquiv s).symm i).2) = ↑i

Reading a packed index back.

@[simp]

theorem MIPRE.Verifier.tagEquiv_apply (s : ℕ) (p : Bool × (Fin s → CL.𝔽₂)) : ↑((tagEquiv s) p) = bitsToIdx (p.1 :: CL.toBits p.2)

def MIPRE.Verifier.accList (s T : ℕ) (acc? : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → Bool) : List (ℕ × ℕ × ℕ × ℕ)

The acceptance table: the index tuples of the answer tuples a predicate accepts, enumerated over the two alphabets.

Equations

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

theorem MIPRE.Verifier.mem_accList_iff {s T : ℕ} {acc? : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → Bool} {i j k l : ℕ} : (i, j, k, l) ∈ accList s T acc? ↔ ∃ x ∈ Cost.Data.bitStrsOfLen s, ∃ y ∈ Cost.Data.bitStrsOfLen s, ∃ a ∈ Cost.Data.bitStrsLE T, ∃ b ∈ Cost.Data.bitStrsLE T, acc? x y a b = true ∧ i = bitsToIdx x ∧ j = bitsToIdx y ∧ k = List.idxOf a (Cost.Data.bitStrsLE T) ∧ l = List.idxOf b (Cost.Data.bitStrsLE T)

The acceptance table is primitive recursive

Written as four nested Primrec.list_flatMap the proof diverges at whnf: each body carries the accumulated parameter tuple and unification grows with it. Flattening the product first makes every flatMap body a bare tuple constructor, and the table is then one filterMap over the flat list (accList_eq_filterMap) — with Verifier.accList itself unchanged.

def MIPRE.Verifier.tuples (s T : ℕ) : List (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr)

The four-fold product of the two enumerations, as one flat list.

Equations

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

theorem MIPRE.Verifier.primrec_tuples : Primrec₂ tuples

def MIPRE.Verifier.accListW (s T : ℕ) (fA fB : Cost.BitStr → ℕ) (acc? : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → Bool) : List (ℕ × ℕ × ℕ × ℕ)

Equations

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

theorem MIPRE.Verifier.mem_accListW_iff {s T : ℕ} {fA fB : Cost.BitStr → ℕ} {acc? : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → Bool} {i j k l : ℕ} : (i, j, k, l) ∈ accListW s T fA fB acc? ↔ ∃ x ∈ Cost.Data.bitStrsOfLen s, ∃ y ∈ Cost.Data.bitStrsOfLen s, ∃ a ∈ Cost.Data.bitStrsLE T, ∃ b ∈ Cost.Data.bitStrsLE T, acc? x y a b = true ∧ i = fA x ∧ j = fB y ∧ k = List.idxOf a (Cost.Data.bitStrsLE T) ∧ l = List.idxOf b (Cost.Data.bitStrsLE T)

theorem MIPRE.Verifier.accListW_eq_filterMap (s T : ℕ) (fA fB : Cost.BitStr → ℕ) (acc? : Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → Bool) : accListW s T fA fB acc? = List.filterMap (fun (q : Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) => if acc? q.1 q.2.1 q.2.2.1 q.2.2.2 = true then some (fA q.1, fB q.2.1, List.idxOf q.2.2.1 (Cost.Data.bitStrsLE T), List.idxOf q.2.2.2 (Cost.Data.bitStrsLE T)) else none) (tuples s T)

theorem MIPRE.Verifier.primrec_accListW {α : Type u_1} [Primcodable α] {s T : α → ℕ} {fA fB : Cost.BitStr → ℕ} {acc? : α → Cost.BitStr → Cost.BitStr → Cost.BitStr → Cost.BitStr → Bool} (hs : Primrec s) (hT : Primrec T) (hfA : Primrec fA) (hfB : Primrec fB) (hacc : Primrec fun (q : α × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) => acc? q.1 q.2.1 q.2.2.1 q.2.2.2.1 q.2.2.2.2) : Primrec fun (a : α) => accListW (s a) (T a) fA fB (acc? a)

theorem MIPRE.Verifier.primrec_tagIdxOf (b : Bool) : Primrec fun (z : Cost.BitStr) => bitsToIdx (b :: z)

Prepending a fixed tag bit is primitive recursive.

The tabulation on parameters alone

tabOf sd pd s T B k n is the GameData seven parameters describe: sd the encoded sampler program, pd the encoded decider program, s the sampler's dimension at level n, T the answer-length cut, B and k the coefficient and the degree of the budget the two sampler runs get, and n the level itself. Nothing here mentions a Verifier, and that is the point — a Verifier is a structure carrying proofs, so a function of one is not data, while Primrec needs its input to be. The bridge back, that these parameters compute the verifier's own sampler and decider, is MIPRE.Halting.dimOf_eq, margOf_eq and accOf_iff in Halting/Instantiation.lean — the first two at every string and every level, the third on an n-bounded verifier.

The three components each run one program under a budget, and the budgets differ: dimOf and margOf one sampler query each (CL.Sampler.queryUnder at the B * (|q| + 1) ^ k passed in, which the caller takes from the sampler's own time bound), accOf one decider run (Decider.acceptBudget at T = n ^ n, k = n, the budget n-boundedness supplies — see accOf, which cannot be re-budgeted and says why). Each defaults — to 0, [], false — when the budget is missed or the answer does not decode, which is what makes them total; where the budget is the right one the default is never taken.

The questions are doubled: Alice's index is her marginal's bit string with a false tag prepended, Bob's with a true tag, so nX + 1 = 2 ^ (s + 1) and the acceptance table is Verifier.accListW at those two indexings rather than accList. The packing is the section "The doubled question alphabet, indexed" above; why the doubling is needed at all is in Foundations/GameDouble.lean.

def MIPRE.Halting.dimOf (sd : Cost.Data) (B k n : ℕ) : ℕ

Equations

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

def MIPRE.Halting.margOf (sd : Cost.Data) (B k n : ℕ) (w : Player) (z : Cost.BitStr) : Cost.BitStr

Player w's marginal question at the point z, under the budget B * (|q| + 1) ^ k.

Equations

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

def MIPRE.Halting.accOf (pd : Cost.Data) (n : ℕ) (x y a b : Cost.BitStr) : Bool

Acceptance, from the encoded decider program alone. Unlike the two sampler runs this one cannot be re-budgeted off GapCompression.sampler_time: the decider of the verifier a string denotes is the string's own, wrapped, and nothing bounds it unconditionally. So accOf keeps the budget n-boundedness supplies, and MIPRE.Halting.accOf_iff keeps its hypothesis.

decide (… = some …) rather than … == some …: the BEq a == elaborates to here is not the one Primrec.eq is stated at, and reconciling them is a long detour for no gain.

Equations

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

def MIPRE.Halting.tabOf (sd pd : Cost.Data) (s T B k n : ℕ) : HaltingGameValue.GameData

The tabulation, doubled and re-budgeted. Alice's question index is her marginal's bit string with a false tag prepended, Bob's with a true tag: the two blocks are disjoint and the diagonal carries no weight. The weight list still enumerates 𝔽₂^s once, so the total weight is still 2 ^ s.

Equations

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

theorem MIPRE.Halting.primrec_dimOf {α : Type u_1} [Primcodable α] {sd : α → Cost.Data} {B lvl : α → ℕ} (k : ℕ) (hsd : Primrec sd) (hB : Primrec B) (hlvl : Primrec lvl) : Primrec fun (a : α) => dimOf (sd a) (B a) k (lvl a)

theorem MIPRE.Halting.primrec_margOf {α : Type u_1} [Primcodable α] {sd : α → Cost.Data} {B lvl : α → ℕ} (k : ℕ) (hsd : Primrec sd) (hB : Primrec B) (hlvl : Primrec lvl) (w : Player) : Primrec fun (q : α × Cost.BitStr) => margOf (sd q.1) (B q.1) k (lvl q.1) w q.2

theorem MIPRE.Halting.primrec_weightList {α : Type u_1} [Primcodable α] {sd : α → Cost.Data} {s B lvl : α → ℕ} (k : ℕ) (hsd : Primrec sd) (hs : Primrec s) (hB : Primrec B) (hlvl : Primrec lvl) : Primrec fun (a : α) => Verifier.weightList (s a) (fun (z : Cost.BitStr) => Verifier.bitsToIdx (false :: margOf (sd a) (B a) k (lvl a) Player.alice z)) fun (z : Cost.BitStr) => Verifier.bitsToIdx (true :: margOf (sd a) (B a) k (lvl a) Player.bob z)

The weight list of the doubled, re-budgeted tabulation. Verifier.weightList itself is untouched: only the two index maps it is applied to have changed.

theorem MIPRE.Halting.primrec_accOf {α : Type u_1} [Primcodable α] {pd : α → Cost.Data} {lvl : α → ℕ} (hpd : Primrec pd) (hlvl : Primrec lvl) : Primrec fun (q : α × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) => accOf (pd q.1) (lvl q.1) q.2.1 q.2.2.1 q.2.2.2.1 q.2.2.2.2

primrec_accOf, generic in the ambient parameter type. accOf reads only the decider data and the level, so the shape of the tuple carrying them is irrelevant. Stating it this way is what makes the re-budget cheap: a change to tabOf's parameter list never re-runs this proof, which measures 210049 heartbeats at one fixed tuple, and composing it with a projection to reach a wider one times out at the default budget.

theorem MIPRE.Halting.primrec_tabOf {α : Type u_1} [Primcodable α] {sd pd : α → Cost.Data} {s T B lvl : α → ℕ} (k : ℕ) (hsd : Primrec sd) (hpd : Primrec pd) (hs : Primrec s) (hT : Primrec T) (hB : Primrec B) (hlvl : Primrec lvl) : Primrec fun (a : α) => tabOf (sd a) (pd a) (s a) (T a) (B a) k (lvl a)

O2, computability, on numbers alone: the doubled, re-budgeted tabulation is primitive recursive in every one of its parameters.