The output indicator: the table of the decoupled system, and the check

Paper II's triangulated output indicator L* (Definition defn:decider-read, II:8381) reads the two readable answers a^R, b^R and a bit string O, and accepts when O is the table of the 5-decoupled triangulated purified system of the constraints at the two questions (claim:properties_of_L*, II:8494). This file is its mathematics; the program is MIPRE.Tailored.AnsRed.IndicatorProg.

• The index space [N] × [N] × [D]³ × [64] of the table, the first coordinate fastest (encIdx, idxA, …, idxS): with N = 2^ℓ and D = 2^◇ the binary digits of an index are those of its six coordinates in turn, the paper's embedding into F₂^{2Λ+3◇+6} (II:8453). The last coordinate holds the six signs, one per bit (sgn).
• indTable N D tris: the indicator of the decoupled system (decInd) over the index space, a bit string of length tableSize N D = 64 N² D³ (indTable_eq_indLoop: the output of the loops over the coordinates); TableSat: five assignments satisfy every equation the table contains, the form in which the PCP checks it (fact:polynomial_condition_for_satisfiability, II:8147); tableSat_indTable_iff: on the table of a system whose equations are below D, that is DecSat.
• LstarOK: the check of the output indicator, on the table size N and the copy size D of the index, the four lengths at the two questions and the constraints the processor outputs on the readable answers, for inputs a = a^R O and b = b^R: the lengths are at most N, b has N bits and O has tableSize N D, there are enough triangulation variables, and O is the table. The readable answers are a and b cut at the readable lengths, so the honest answers are padded with zeros (lstarOK_pad).
• claim:properties_of_L*, item 2: accepts_of_lstarOK (a satisfying 5-tuple of the table gives answers the game accepts) and tableSat_of_accepts (answers the game accepts give the satisfying 5-tuple Extend, the last three blocks linear in the linear answers).

Here the input verifier is neither padded nor purified (II:8377, planning/aldous-lyons-track.md §5, "Phase 4 slices"): the readable answers are cut at the readable lengths and the constraints purified on the fly (pureEqn), so the paper's steps 3 and 4 have nothing to check.

The index space

def MIPRE.Tailored.AnsRed.tableSize (N D : ℕ) : ℕ

The number of indices of the table, 64 N² D³.

Equations

• MIPRE.Tailored.AnsRed.tableSize N D = N * (N * (D * (D * (D * 64))))

def MIPRE.Tailored.AnsRed.encIdx (N D uA uB u₁ u₂ u₃ s : ℕ) : ℕ

The index of (u_A, u_B, u₁, u₂, u₃, s) in [N] × [N] × [D]³ × [64], the first coordinate fastest.

Equations

• MIPRE.Tailored.AnsRed.encIdx N D uA uB u₁ u₂ u₃ s = uA + N * (uB + N * (u₁ + D * (u₂ + D * (u₃ + D * s))))

def MIPRE.Tailored.AnsRed.idxA (N u : ℕ) : ℕ

The first coordinate of an index, in the block S_A.

Equations

• MIPRE.Tailored.AnsRed.idxA N u = u % N

def MIPRE.Tailored.AnsRed.idxB (N u : ℕ) : ℕ

The second coordinate, in the block S_B.

Equations

• MIPRE.Tailored.AnsRed.idxB N u = u / N % N

def MIPRE.Tailored.AnsRed.idx₁ (N D u : ℕ) : ℕ

The third coordinate, in the first copy.

Equations

• MIPRE.Tailored.AnsRed.idx₁ N D u = u / N / N % D

def MIPRE.Tailored.AnsRed.idx₂ (N D u : ℕ) : ℕ

The fourth coordinate, in the second copy.

Equations

• MIPRE.Tailored.AnsRed.idx₂ N D u = u / N / N / D % D

def MIPRE.Tailored.AnsRed.idx₃ (N D u : ℕ) : ℕ

The fifth coordinate, in the third copy.

Equations

• MIPRE.Tailored.AnsRed.idx₃ N D u = u / N / N / D / D % D

def MIPRE.Tailored.AnsRed.idxS (N D u : ℕ) : ℕ

The last coordinate, the six signs.

Equations

• MIPRE.Tailored.AnsRed.idxS N D u = u / N / N / D / D / D

theorem MIPRE.Tailored.AnsRed.encIdx_lt {N D uA uB u₁ u₂ u₃ s : ℕ} (hA : uA < N) (hB : uB < N) (h₁ : u₁ < D) (h₂ : u₂ < D) (h₃ : u₃ < D) (hs : s < 64) : encIdx N D uA uB u₁ u₂ u₃ s < tableSize N D

theorem MIPRE.Tailored.AnsRed.idxA_encIdx {N D uA uB u₁ u₂ u₃ s : ℕ} (hA : uA < N) : idxA N (encIdx N D uA uB u₁ u₂ u₃ s) = uA

theorem MIPRE.Tailored.AnsRed.idxB_encIdx {N D uA uB u₁ u₂ u₃ s : ℕ} (hA : uA < N) (hB : uB < N) : idxB N (encIdx N D uA uB u₁ u₂ u₃ s) = uB

theorem MIPRE.Tailored.AnsRed.idx₁_encIdx {N D uA uB u₁ u₂ u₃ s : ℕ} (hA : uA < N) (hB : uB < N) (h₁ : u₁ < D) : idx₁ N D (encIdx N D uA uB u₁ u₂ u₃ s) = u₁

theorem MIPRE.Tailored.AnsRed.idx₂_encIdx {N D uA uB u₁ u₂ u₃ s : ℕ} (hA : uA < N) (hB : uB < N) (h₁ : u₁ < D) (h₂ : u₂ < D) : idx₂ N D (encIdx N D uA uB u₁ u₂ u₃ s) = u₂

theorem MIPRE.Tailored.AnsRed.idx₃_encIdx {N D uA uB u₁ u₂ u₃ s : ℕ} (hA : uA < N) (hB : uB < N) (h₁ : u₁ < D) (h₂ : u₂ < D) (h₃ : u₃ < D) : idx₃ N D (encIdx N D uA uB u₁ u₂ u₃ s) = u₃

theorem MIPRE.Tailored.AnsRed.idxS_encIdx {N D uA uB u₁ u₂ u₃ s : ℕ} (hA : uA < N) (hB : uB < N) (h₁ : u₁ < D) (h₂ : u₂ < D) (h₃ : u₃ < D) : idxS N D (encIdx N D uA uB u₁ u₂ u₃ s) = s

The signs

def MIPRE.Tailored.AnsRed.sgn (s i : ℕ) : ZMod 2

The i-th sign held by the last coordinate s: its i-th binary digit.

Equations

• MIPRE.Tailored.AnsRed.sgn s i = MIPRE.LowDegree.ofBool (s.testBit i)

def MIPRE.Tailored.AnsRed.sgnIdx (e₀ e₁ e₂ e₃ e₄ e₅ : ZMod 2) : ℕ

The last coordinate holding six given signs.

Equations

• MIPRE.Tailored.AnsRed.sgnIdx e₀ e₁ e₂ e₃ e₄ e₅ = e₀.val + 2 * e₁.val + 4 * e₂.val + 8 * e₃.val + 16 * e₄.val + 32 * e₅.val

theorem MIPRE.Tailored.AnsRed.sgnIdx_lt (e₀ e₁ e₂ e₃ e₄ e₅ : ZMod 2) : sgnIdx e₀ e₁ e₂ e₃ e₄ e₅ < 64

theorem MIPRE.Tailored.AnsRed.sgn_sgnIdx (e₀ e₁ e₂ e₃ e₄ e₅ : ZMod 2) : sgn (sgnIdx e₀ e₁ e₂ e₃ e₄ e₅) 0 = e₀ ∧ sgn (sgnIdx e₀ e₁ e₂ e₃ e₄ e₅) 1 = e₁ ∧ sgn (sgnIdx e₀ e₁ e₂ e₃ e₄ e₅) 2 = e₂ ∧ sgn (sgnIdx e₀ e₁ e₂ e₃ e₄ e₅) 3 = e₃ ∧ sgn (sgnIdx e₀ e₁ e₂ e₃ e₄ e₅) 4 = e₄ ∧ sgn (sgnIdx e₀ e₁ e₂ e₃ e₄ e₅) 5 = e₅

The table

def MIPRE.Tailored.AnsRed.IndAt (N D : ℕ) (tris : List Tri) (u : ℕ) : Prop

Whether the equation at the index u is in the decoupled system of tris on the blocks [N], [N] and three copies of [D].

Equations

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

@[instance_reducible]

instance MIPRE.Tailored.AnsRed.instDecidableIndAt (N D : ℕ) (tris : List Tri) (u : ℕ) : Decidable (IndAt N D tris u)

Equations

• MIPRE.Tailored.AnsRed.instDecidableIndAt N D tris u = id inferInstance

def MIPRE.Tailored.AnsRed.indTable (N D : ℕ) (tris : List Tri) : Cost.BitStr

The table of the decoupled system (II:8453, rem:alg_5-decoupling): its indicator over the index space, a bit string of length 64 N² D³.

Equations

• MIPRE.Tailored.AnsRed.indTable N D tris = List.ofFn fun (u : Fin (MIPRE.Tailored.AnsRed.tableSize N D)) => decide (MIPRE.Tailored.AnsRed.IndAt N D tris ↑u)

@[simp]

theorem MIPRE.Tailored.AnsRed.length_indTable (N D : ℕ) (tris : List Tri) : List.length (indTable N D tris) = tableSize N D

theorem MIPRE.Tailored.AnsRed.getD_indTable {N D : ℕ} {tris : List Tri} {u : ℕ} (hu : u < tableSize N D) : List.getD (indTable N D tris) u false = decide (IndAt N D tris u)

The table, loop by loop

theorem MIPRE.Tailored.AnsRed.getElem?_flatMap_const {α : Type u_1} {β : Type u_2} (l : List α) (F : α → List β) {m : ℕ} (hF : ∀ a ∈ l, (F a).length = m) (i : ℕ) {j : ℕ} (hj : j < m) : (List.flatMap F l)[j + m * i]? = l[i]?.bind fun (a : α) => (F a)[j]?

theorem MIPRE.Tailored.AnsRed.length_flatMap_const {α : Type u_1} {β : Type u_2} (l : List α) (F : α → List β) {m : ℕ} (hF : ∀ a ∈ l, (F a).length = m) : (List.flatMap F l).length = m * l.length

def MIPRE.Tailored.AnsRed.indLoop (N D : ℕ) (tris : List Tri) : Cost.BitStr

The table at given signs and coordinates, as the loops visit them.

Equations

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

theorem MIPRE.Tailored.AnsRed.indTable_eq_indLoop (N D : ℕ) (tris : List Tri) : indTable N D tris = indLoop N D tris

The table is the loops' output: the sign words outermost, the first coordinate innermost, the order of the index space.

def MIPRE.Tailored.AnsRed.EqAt (N D u : ℕ) (fA fB f₁ f₂ f₃ : ℕ → ZMod 2) : Prop

The equation at the index u, on five assignments.

Equations

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

def MIPRE.Tailored.AnsRed.TableSat (N D : ℕ) (O : Cost.BitStr) (fA fB f₁ f₂ f₃ : ℕ → ZMod 2) : Prop

Five assignments satisfy the system a table holds (fact:polynomial_condition_for_satisfiability): every equation whose index the table contains holds.

Equations

• MIPRE.Tailored.AnsRed.TableSat N D O fA fB f₁ f₂ f₃ = ∀ u < MIPRE.Tailored.AnsRed.tableSize N D, List.getD O u false = true → MIPRE.Tailored.AnsRed.EqAt N D u fA fB f₁ f₂ f₃

theorem MIPRE.Tailored.AnsRed.tableSat_indTable_iff {N D : ℕ} {tris : List Tri} (hN : 0 < N) (hND : N + N ≤ D) (hbel : ∀ t ∈ tris, t.Below D) {fA fB f₁ f₂ f₃ : ℕ → ZMod 2} : TableSat N D (indTable N D tris) fA fB f₁ f₂ f₃ ↔ DecSat N N D tris fA fB f₁ f₂ f₃

The table holds the decoupled system (fact:polynomial_condition_for_satisfiability): on blocks [N], [N] with N > 0 and copies of [D] ⊇ [2N], five assignments satisfy the table of a system whose equations are below D exactly when they satisfy the system.

The check of the output indicator

def MIPRE.Tailored.AnsRed.lsRows (N lRx lLx lRy lLy : ℕ) (aR bR : Cost.BitStr) (cs : List Cost.BitStr) : List Eqn

The rows the output indicator decouples: the purified equations of the constraints cs at the lengths lRx, lLx, lRy, lLy, the linear answers in tables of N entries.

Equations

• MIPRE.Tailored.AnsRed.lsRows N lRx lLx lRy lLy aR bR cs = List.map (MIPRE.Tailored.AnsRed.pureEqn lRx lLx lRy lLy N aR bR) cs

def MIPRE.Tailored.AnsRed.lsTable (N D lRx lLx lRy lLy : ℕ) (aR bR : Cost.BitStr) (cs : List Cost.BitStr) : Cost.BitStr

The table the output indicator expects: that of the decoupled triangulation of the rows, on copies of [D].

Equations

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

def MIPRE.Tailored.AnsRed.LstarOK (N D lRx lLx lRy lLy : ℕ) (cs : List Cost.BitStr) (a b : Cost.BitStr) : Prop

The check of the output indicator (Definition defn:decider-read), at the table size N and the copy size D of the index, the lengths lRx, lLx and lRy, lLy at the two questions, and the constraints cs that the processor outputs on the readable answers a^R, b^R — the inputs a = a^R O and b = b^R cut at the readable lengths: the lengths are at most N (step 1), b has N bits and O has tableSize N D (steps 1 and 8), there are enough triangulation variables (step 5), and O is the table of the decoupled triangulated purified system (steps 6 to 8).

Equations

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

@[instance_reducible]

instance MIPRE.Tailored.AnsRed.instDecidableLstarOK (N D lRx lLx lRy lLy : ℕ) (cs : List Cost.BitStr) (a b : Cost.BitStr) : Decidable (LstarOK N D lRx lLx lRy lLy cs a b)

Equations

• MIPRE.Tailored.AnsRed.instDecidableLstarOK N D lRx lLx lRy lLy cs a b = id inferInstance

theorem MIPRE.Tailored.AnsRed.lstarOK_pad {N D lRx lLx lRy lLy : ℕ} {cs : List Cost.BitStr} {aR bR : Cost.BitStr} (haR : List.length aR = lRx) (hbR : List.length bR = lRy) (hRx : lRx ≤ N) (hLx : lLx ≤ N) (hRy : lRy ≤ N) (hLy : lLy ≤ N) (hD : cs.length * (N + N) + (N + N) ≤ D) : LstarOK N D lRx lLx lRy lLy cs (aR ++ List.replicate (N - lRx) false ++ lsTable N D lRx lLx lRy lLy aR bR cs) (bR ++ List.replicate (N - lRy) false)

claim:properties_of_L, item 1*: the check passes on readable answers of the readable lengths, padded with zeros to N bits, the first followed by the table — the one string O it accepts after them.

def MIPRE.Tailored.AnsRed.lstarCheck (ℓ dm lRx lLx lRy lLy : ℕ) (cs : List Cost.BitStr) (a b : Cost.BitStr) : Bool

The check as the program makes it, on the exponents ℓ and ◇ of the table size and the copy size: the table size is read off b and checked to be 2^ℓ, and the copy size is 2^◇ capped at one more than the length of O, so that no power of two larger than the input is ever written out. It decides LstarOK at (2^ℓ, 2^◇) (lstarCheck_eq).

Equations

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

theorem MIPRE.Tailored.AnsRed.le_tableSize {N D : ℕ} (hN : 0 < N) : D ≤ tableSize N D

theorem MIPRE.Tailored.AnsRed.lstarCheck_eq (ℓ dm lRx lLx lRy lLy : ℕ) (cs : List Cost.BitStr) (a b : Cost.BitStr) : lstarCheck ℓ dm lRx lLx lRy lLy cs a b = decide (LstarOK (2 ^ ℓ) (2 ^ dm) lRx lLx lRy lLy cs a b)

The program's check decides LstarOK at the table size 2^ℓ and the copy size 2^◇.

theorem MIPRE.Tailored.AnsRed.lsRows_eq_pureRows {X : Type u_1} [Fintype X] (G : TailoredGame X) {x y : X} {N lRx lLx lRy lLy : ℕ} {aR bR : Cost.BitStr} {cs : List Cost.BitStr} (hRx : G.lenR x = lRx) (hLx : G.lenL x = lLx) (hRy : G.lenR y = lRy) (hLy : G.lenL y = lLy) (hcs : G.cons x y aR bR = cs) : lsRows N lRx lLx lRy lLy aR bR cs = pureRows G N x y aR bR

theorem MIPRE.Tailored.AnsRed.accepts_of_lstarOK {X : Type u_1} [Fintype X] (G : TailoredGame X) {x y : X} {N D lRx lLx lRy lLy : ℕ} {cs : List Cost.BitStr} {a b : Cost.BitStr} (hRx : G.lenR x = lRx) (hLx : G.lenL x = lLx) (hRy : G.lenR y = lRy) (hLy : G.lenL y = lLy) (hcs : G.cons x y (List.take lRx a) (List.take lRy b) = cs) (hN : 0 < N) (h : LstarOK N D lRx lLx lRy lLy cs a b) {fA fB f₁ f₂ f₃ : ℕ → ZMod 2} (hsat : TableSat N D (List.drop N a) fA fB f₁ f₂ f₃) : G.Accepts x y (List.take lRx a ++ readBlock lLx fA) (List.take lRy b ++ readBlock lLy fB)

claim:properties_of_L, item 2, from the table to the game*: when the check passes on the lengths and constraints of the game at (x, y), five assignments satisfying the table held by a give answers that the game accepts — the readable answers completed by the first two blocks, read at the linear lengths.

theorem MIPRE.Tailored.AnsRed.tableSat_of_accepts {X : Type u_1} [Fintype X] (G : TailoredGame X) {x y : X} {N D : ℕ} {aR aL bR bL : Cost.BitStr} (haR : List.length aR = G.lenR x) (haL : List.length aL = G.lenL x) (hbR : List.length bR = G.lenR y) (hbL : List.length bL = G.lenL y) (hN : 0 < N) (hx : G.lenL x ≤ N) (hy : G.lenL y ≤ N) (hD : (G.cons x y aR bR).length * (N + N) + (N + N) ≤ D) (hacc : G.Accepts x y (aR ++ aL) (bR ++ bL)) : TableSat N D (lsTable N D (G.lenR x) (G.lenL x) (G.lenR y) (G.lenL y) aR bR (G.cons x y aR bR)) (tbl N aL bL) (fun (j : ℕ) => tbl N aL bL (N + j)) (ext (N + N) (pureRows G N x y aR bR) (tbl N aL bL)) (ext (N + N) (pureRows G N x y aR bR) (tbl N aL bL)) (ext (N + N) (pureRows G N x y aR bR) (tbl N aL bL))

claim:properties_of_L, item 2, from the game to the table*: answers of the right lengths that the game accepts give the satisfying 5-tuple Extend of the table — the table of the linear answers, and three times its extension, linear in the linear answers with coefficients read from the readable ones.