Linear systems over F₂: purification, triangulation and decoupling

Slice P4a of the Aldous–Lyons track (planning/aldous-lyons-track.md, §5 "Phase 4 slices"): the transformations of a system of linear equations that paper II's answer reduction applies before its PCP (II:7751–8316). The output indicator L* (II:8381) computes them from the constraints of the input game, and the PCP checks the result.

• Eqn: an equation ∑_{v ∈ vars} X_v = rhs over F₂, on variables indexed by ℕ.
• pureEqn (eq:purified_equation, II:7762): a constraint of the canonical decider on the answers a = a^R a^L, b = b^R b^L becomes an equation on the linear answers alone, the readable values moved to the right-hand side, the linear answers placed in a table of 2L entries (a^L at 0, b^L at L). accepts_iff_pure: the tailored game accepts exactly when the purified equations hold of the table. The paper purifies the input verifier first (II:7783); here the indicator purifies on the fly, so the input is not transformed.
• triangle (II:7952): each equation X_{x₀} + ⋯ + X_{x_{k-1}} = b becomes the chain X_{x₀} = Y₀, Y_{i-1} + X_{xᵢ} = Yᵢ, Y_{k-1} = b of equations in at most three variables, each row with its own fresh variables Y (yv). ext extends an assignment to the fresh variables by the partial sums, a linear map (ext is a sum over extVars); triangle_complete and triangle_sound are the correspondence of solutions (rem:prop_triangulated_system).
• decInd (II:8193, and the indicator encoding of II:8128): the 5-decoupled system on the blocks S_A, S_B, S₁, S₂, S₃, the last three copies of all the variables, as the indicator of the equations ε_A X_A + ε_B X_B + ε₁ X¹ + ε₂ X² + ε₃ X³ = ε₀ it contains; a block whose sign is 0 takes any index. decSat_iff reads off what a solution is.
• extend_complete, decSat_sound (cor:triang_and_decoupling_extend): a solution f gives the solution (f, f(ℓ_A + ·), ext f, ext f, ext f) of the decoupled triangulated system, and the first two blocks of any solution glue to a solution of the original system. accepts_iff_decSat and accepts_of_decSat are the two directions for the canonical decider (claim:properties_of_L*, item 2).

Bits as elements of F₂

def MIPRE.Tailored.AnsRed.bitAt (s : Cost.BitStr) (i : ℕ) : ZMod 2

The bit of s at i as an element of F₂, 0 past the end.

Equations

• MIPRE.Tailored.AnsRed.bitAt s i = MIPRE.LowDegree.ofBool (List.getD s i false)

@[simp]

theorem MIPRE.Tailored.AnsRed.bitAt_cons_zero (x : Bool) (s : Cost.BitStr) : bitAt (x :: s) 0 = LowDegree.ofBool x

@[simp]

theorem MIPRE.Tailored.AnsRed.bitAt_cons_succ (x : Bool) (s : Cost.BitStr) (i : ℕ) : bitAt (x :: s) (i + 1) = bitAt s i

theorem MIPRE.Tailored.AnsRed.bitAt_append_left {s t : Cost.BitStr} {i : ℕ} (h : i < List.length s) : bitAt (s ++ t) i = bitAt s i

theorem MIPRE.Tailored.AnsRed.bitAt_append_right (s t : Cost.BitStr) (i : ℕ) : bitAt (s ++ t) (List.length s + i) = bitAt t i

theorem MIPRE.Tailored.AnsRed.ofBool_dotL (c v : Cost.BitStr) : List.length c = List.length v → LowDegree.ofBool (Intro.dotL c v) = ∑ j ∈ Finset.range (List.length c), bitAt c j * bitAt v j

The F₂ inner product of two strings of the same length, as a sum.

theorem MIPRE.Tailored.AnsRed.sum_map_filter_range (k : ℕ) (p : ℕ → Bool) (g : ℕ → ZMod 2) : (List.map g (List.filter p (List.range k))).sum = ∑ j ∈ Finset.range k, if p j = true then g j else 0

A sum over the positions of a filtered range.

Equations

structure MIPRE.Tailored.AnsRed.Eqn : Type

A linear equation over F₂, ∑_{v ∈ vars} X_v = rhs, on variables indexed by ℕ.

• vars : List ℕ

  The variables with coefficient 1 (with multiplicity, which is counted mod 2).

• rhs : ZMod 2

  The right-hand side.

def MIPRE.Tailored.AnsRed.Eqn.Holds (e : Eqn) (f : ℕ → ZMod 2) : Prop

An assignment satisfies the equation.

Equations

• e.Holds f = ((List.map f e.vars).sum = e.rhs)

def MIPRE.Tailored.AnsRed.Eqn.Below (e : Eqn) (N : ℕ) : Prop

The equation mentions only variables below N.

Equations

• e.Below N = ∀ v ∈ e.vars, v < N

theorem MIPRE.Tailored.AnsRed.Eqn.holds_congr {e : Eqn} {N : ℕ} (he : e.Below N) {f g : ℕ → ZMod 2} (hfg : ∀ v < N, f v = g v) : e.Holds f ↔ e.Holds g

An equation below N holds of two assignments that agree below N together.

Purification

def MIPRE.Tailored.AnsRed.onesFrom (c : Cost.BitStr) (o k : ℕ) : List ℕ

The positions j < k at which c has a one at o + j.

Equations

• MIPRE.Tailored.AnsRed.onesFrom c o k = List.filter (fun (j : ℕ) => List.getD c (o + j) false) (List.range k)

theorem MIPRE.Tailored.AnsRed.mem_onesFrom {c : Cost.BitStr} {o k j : ℕ} (h : j ∈ onesFrom c o k) : j < k

theorem MIPRE.Tailored.AnsRed.length_onesFrom_le (c : Cost.BitStr) (o k : ℕ) : (onesFrom c o k).length ≤ k

theorem MIPRE.Tailored.AnsRed.sum_map_onesFrom (c : Cost.BitStr) (o k : ℕ) (g : ℕ → ZMod 2) : (List.map g (onesFrom c o k)).sum = ∑ j ∈ Finset.range k, bitAt c (o + j) * g j

def MIPRE.Tailored.AnsRed.tbl (L : ℕ) (aL bL : Cost.BitStr) (v : ℕ) : ZMod 2

The linear answers placed in a table of 2L entries: a^L at 0, b^L at L.

Equations

• MIPRE.Tailored.AnsRed.tbl L aL bL v = if v < L then MIPRE.Tailored.AnsRed.bitAt aL v else MIPRE.Tailored.AnsRed.bitAt bL (v - L)

def MIPRE.Tailored.AnsRed.pureEqn (lRx lLx lRy lLy L : ℕ) (aR bR c : Cost.BitStr) : Eqn

The purified equation of a constraint c (eq:purified_equation): the constraint on the answers a^R a^L (lengths lRx, lLx) and b^R b^L (lengths lRy, lLy) and the affine coordinate becomes an equation on the table tbl L a^L b^L of the linear answers, the readable answers a^R, b^R entering the right-hand side. A constraint of the wrong length, which the canonical decider rejects, becomes 0 = 1.

Equations

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

theorem MIPRE.Tailored.AnsRed.mem_pureEqn_vars {lRx lLx lRy lLy L : ℕ} {aR bR c : Cost.BitStr} {v : ℕ} (hv : v ∈ (pureEqn lRx lLx lRy lLy L aR bR c).vars) : v < lLx ∨ L ≤ v ∧ v - L < lLy

The purified equation mentions only the positions of the two linear answers in the table.

theorem MIPRE.Tailored.AnsRed.pureEqn_below {lRx lLx lRy lLy L : ℕ} (hx : lLx ≤ L) (hy : lLy ≤ L) (aR bR c : Cost.BitStr) : (pureEqn lRx lLx lRy lLy L aR bR c).Below (2 * L)

theorem MIPRE.Tailored.AnsRed.length_pureEqn_le {lRx lLx lRy lLy L : ℕ} (hx : lLx ≤ L) (hy : lLy ≤ L) (aR bR c : Cost.BitStr) : (pureEqn lRx lLx lRy lLy L aR bR c).vars.length ≤ 2 * L

theorem MIPRE.Tailored.AnsRed.satisfies_iff_pureEqn {lRx lLx lRy lLy L : ℕ} {aR aL bR bL : Cost.BitStr} (haR : List.length aR = lRx) (haL : List.length aL = lLx) (hbR : List.length bR = lRy) (hbL : List.length bL = lLy) (hx : lLx ≤ L) (c : Cost.BitStr) : Satisfies c (aR ++ aL ++ (bR ++ bL) ++ [true]) ↔ (pureEqn lRx lLx lRy lLy L aR bR c).Holds (tbl L aL bL)

Purification is exact (fact:completeness_and_soundness_purification, at one pair of answers): the constraint holds of the answers exactly when its purified equation holds of the table of their linear parts.

theorem MIPRE.Tailored.AnsRed.accepts_iff_pure {X : Type u_1} [Fintype X] (G : TailoredGame X) (x y : X) {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) {L : ℕ} (hx : G.lenL x ≤ L) : G.Accepts x y (aR ++ aL) (bR ++ bL) ↔ ∀ e ∈ List.map (pureEqn (G.lenR x) (G.lenL x) (G.lenR y) (G.lenL y) L aR bR) (G.cons x y aR bR), e.Holds (tbl L aL bL)

The canonical decider, purified: a tailored game accepts answers a^R a^L, b^R b^L of the right lengths exactly when the purified equations of its constraints hold of the table of the linear answers.

Triangulation

structure MIPRE.Tailored.AnsRed.Tri : Type

A triangulated equation a₁ X_{v₁} + a₂ X_{v₂} + a₃ X_{v₃} = b: at most three variables, in three slots, which the decoupling sends to three different copies of the variables. A slot with coefficient 0 is unused, whatever its index.

• v₁ : ℕ
• v₂ : ℕ
• v₃ : ℕ
• a₁ : ZMod 2
• a₂ : ZMod 2
• a₃ : ZMod 2
• b : ZMod 2

def MIPRE.Tailored.AnsRed.Tri.Holds3 (t : Tri) (f₁ f₂ f₃ : ℕ → ZMod 2) : Prop

The equation holds of three assignments, one per slot.

Equations

• t.Holds3 f₁ f₂ f₃ = (t.a₁ * f₁ t.v₁ + t.a₂ * f₂ t.v₂ + t.a₃ * f₃ t.v₃ = t.b)

def MIPRE.Tailored.AnsRed.Tri.Holds (t : Tri) (f : ℕ → ZMod 2) : Prop

The equation holds of one assignment.

Equations

• t.Holds f = t.Holds3 f f f

def MIPRE.Tailored.AnsRed.Tri.Below (t : Tri) (ℓ : ℕ) : Prop

The variables of the used slots are below ℓ.

Equations

• t.Below ℓ = ((t.a₁ ≠ 0 → t.v₁ < ℓ) ∧ (t.a₂ ≠ 0 → t.v₂ < ℓ) ∧ (t.a₃ ≠ 0 → t.v₃ < ℓ))

theorem MIPRE.Tailored.AnsRed.Tri.holds3_iff_holds {t : Tri} {ℓ : ℕ} (ht : t.Below ℓ) {f₁ f₂ f₃ : ℕ → ZMod 2} (h₁₂ : ∀ j < ℓ, f₁ j = f₂ j) (h₂₃ : ∀ j < ℓ, f₂ j = f₃ j) : t.Holds3 f₁ f₂ f₃ ↔ t.Holds f₁

On three assignments that agree below ℓ, an equation below ℓ holds of all three iff it holds of the first.

def MIPRE.Tailored.AnsRed.yv (N r i : ℕ) : ℕ

The fresh variable Y_{r,i} of the triangulation: rows of stride N after the N original variables.

Equations

• MIPRE.Tailored.AnsRed.yv N r i = N + r * N + i

theorem MIPRE.Tailored.AnsRed.yv_sub_div {N r i : ℕ} (hi : i < N) : (yv N r i - N) / N = r

theorem MIPRE.Tailored.AnsRed.yv_sub_mod {N r i : ℕ} (hi : i < N) : (yv N r i - N) % N = i

theorem MIPRE.Tailored.AnsRed.le_yv (N r i : ℕ) : N ≤ yv N r i

def MIPRE.Tailored.AnsRed.triRow (N r : ℕ) (e : Eqn) : List Tri

The triangulation of the equation e, the r-th row: the step equations X_{xᵢ} + Y_{r,i-1} + Y_{r,i} = 0 (no Y_{r,-1} at i = 0), then Y_{r,k-1} = rhs (just 0 = rhs when k = 0).

Equations

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

def MIPRE.Tailored.AnsRed.triangle (N : ℕ) (rows : List Eqn) : List Tri

The triangulated system (II:7952): the rows triangulated one by one.

Equations

• MIPRE.Tailored.AnsRed.triangle N rows = (List.mapIdx (fun (r : ℕ) (e : MIPRE.Tailored.AnsRed.Eqn) => MIPRE.Tailored.AnsRed.triRow N r e) rows).flatten

theorem MIPRE.Tailored.AnsRed.mem_triangle {N : ℕ} {rows : List Eqn} {t : Tri} : t ∈ triangle N rows ↔ ∃ (r : ℕ) (h : r < rows.length), t ∈ triRow N r rows[r]

def MIPRE.Tailored.AnsRed.extVars (N : ℕ) (rows : List Eqn) (v : ℕ) : List ℕ

The variables whose sum is the extended assignment at v: v itself below N, the prefix x₀, …, xᵢ of the r-th row at Y_{r,i}, nothing elsewhere.

Equations

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

def MIPRE.Tailored.AnsRed.ext (N : ℕ) (rows : List Eqn) (f : ℕ → ZMod 2) (v : ℕ) : ZMod 2

The extension of an assignment to the triangulation variables (rem:prop_triangulated_system, item 1): the partial sums along each row. It is linear, being a sum over extVars.

Equations

• MIPRE.Tailored.AnsRed.ext N rows f v = (List.map f (MIPRE.Tailored.AnsRed.extVars N rows v)).sum

theorem MIPRE.Tailored.AnsRed.extVars_below {N : ℕ} {rows : List Eqn} (hbel : ∀ e ∈ rows, e.Below N) (v u : ℕ) : u ∈ extVars N rows v → u < N

The extension reads only the original variables.

theorem MIPRE.Tailored.AnsRed.ext_of_lt {N : ℕ} {rows : List Eqn} {v : ℕ} (hv : v < N) (f : ℕ → ZMod 2) : ext N rows f v = f v

theorem MIPRE.Tailored.AnsRed.ext_yv {N : ℕ} {rows : List Eqn} {r i : ℕ} (hr : r < rows.length) (hi : i < N) (hk : i < rows[r].vars.length) (f : ℕ → ZMod 2) : ext N rows f (yv N r i) = (List.map f (List.take (i + 1) rows[r].vars)).sum

theorem MIPRE.Tailored.AnsRed.triangle_complete {N : ℕ} {rows : List Eqn} (hlen : ∀ e ∈ rows, e.vars.length ≤ N) (hbel : ∀ e ∈ rows, e.Below N) {f : ℕ → ZMod 2} (hf : ∀ e ∈ rows, e.Holds f) (t : Tri) : t ∈ triangle N rows → t.Holds (ext N rows f)

Triangulation is complete: the extension of a solution solves the triangulated system, when the rows have at most N variables, all below N.

theorem MIPRE.Tailored.AnsRed.triangle_sound {N : ℕ} {rows : List Eqn} {g : ℕ → ZMod 2} (hg : ∀ t ∈ triangle N rows, t.Holds g) (e : Eqn) : e ∈ rows → e.Holds g

Triangulation is sound: a solution of the triangulated system solves every row.

theorem MIPRE.Tailored.AnsRed.triangle_below {N Δ : ℕ} {rows : List Eqn} (hlen : ∀ e ∈ rows, e.vars.length ≤ N) (hbel : ∀ e ∈ rows, e.Below N) (hΔ : rows.length * N ≤ Δ) (t : Tri) : t ∈ triangle N rows → t.Below (N + Δ)

Every equation of the triangulated system of R rows of at most N variables, all below N, is below N + Δ when R N ≤ Δ.

Decoupling

def MIPRE.Tailored.AnsRed.decInd (ℓA ℓB ℓ : ℕ) (tris : List Tri) (uA uB u₁ u₂ u₃ : ℕ) (εA εB ε₁ ε₂ ε₃ ε₀ : ZMod 2) : Prop

The indicator of the 5-decoupled system (II:8193, encoded as in II:8128): whether the equation ε_A X_A(u_A) + ε_B X_B(u_B) + ε₁ X¹(u₁) + ε₂ X²(u₂) + ε₃ X³(u₃) = ε₀ is in the system on the blocks S_A = [ℓ_A], S_B = [ℓ_B] and three copies S₁, S₂, S₃ of [ℓ], whose equations are X_A = X¹ on S_A, X_B = X¹(ℓ_A + ·) on S_B, X¹ = X² and X² = X³ on [ℓ], and each triangulated equation of tris on the three copies. A block whose sign is 0 takes any index.

Equations

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

@[instance_reducible]

instance MIPRE.Tailored.AnsRed.instDecidableDecInd (ℓA ℓB ℓ : ℕ) (tris : List Tri) (uA uB u₁ u₂ u₃ : ℕ) (εA εB ε₁ ε₂ ε₃ ε₀ : ZMod 2) : Decidable (decInd ℓA ℓB ℓ tris uA uB u₁ u₂ u₃ εA εB ε₁ ε₂ ε₃ ε₀)

Equations

• MIPRE.Tailored.AnsRed.instDecidableDecInd ℓA ℓB ℓ tris uA uB u₁ u₂ u₃ εA εB ε₁ ε₂ ε₃ ε₀ = id inferInstance

def MIPRE.Tailored.AnsRed.DecSat (ℓA ℓB ℓ : ℕ) (tris : List Tri) (fA fB f₁ f₂ f₃ : ℕ → ZMod 2) : Prop

Five assignments satisfy the decoupled system (fact:polynomial_condition_for_satisfiability): every equation of the indicator holds.

Equations

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

theorem MIPRE.Tailored.AnsRed.decSat_iff {ℓA ℓB ℓ : ℕ} {tris : List Tri} {fA fB f₁ f₂ f₃ : ℕ → ZMod 2} : DecSat ℓA ℓB ℓ tris fA fB f₁ f₂ f₃ ↔ (∀ j < ℓA, fA j = f₁ j) ∧ (∀ j < ℓB, fB j = f₁ (ℓA + j)) ∧ (∀ j < ℓ, f₁ j = f₂ j) ∧ (∀ j < ℓ, f₂ j = f₃ j) ∧ ∀ t ∈ tris, t.Holds3 f₁ f₂ f₃

What a solution of the decoupled system is: the copy equations and the triangulated equations on the three copies.

Triangulation and decoupling together

def MIPRE.Tailored.AnsRed.glue (ℓA : ℕ) (fA fB : ℕ → ZMod 2) (v : ℕ) : ZMod 2

The two first blocks glued into one assignment of the original variables: f_A below ℓ_A, f_B shifted above.

Equations

• MIPRE.Tailored.AnsRed.glue ℓA fA fB v = if v < ℓA then fA v else fB (v - ℓA)

theorem MIPRE.Tailored.AnsRed.extend_complete {ℓA ℓB Δ : ℕ} {rows : List Eqn} (hlen : ∀ e ∈ rows, e.vars.length ≤ ℓA + ℓB) (hbel : ∀ e ∈ rows, e.Below (ℓA + ℓB)) {f : ℕ → ZMod 2} (hf : ∀ e ∈ rows, e.Holds f) : DecSat ℓA ℓB (ℓA + ℓB + Δ) (triangle (ℓA + ℓB) rows) f (fun (j : ℕ) => f (ℓA + j)) (ext (ℓA + ℓB) rows f) (ext (ℓA + ℓB) rows f) (ext (ℓA + ℓB) rows f)

Extend is complete (cor:triang_and_decoupling_extend): a solution f of R rows of at most N = ℓ_A + ℓ_B variables, all below N, gives the solution (f, f(ℓ_A + ·), ext f, ext f, ext f) of the decoupled triangulated system with Δ ≥ R N triangulation variables. The last three blocks are linear in f (ext).

theorem MIPRE.Tailored.AnsRed.decSat_sound {ℓA ℓB Δ : ℕ} {rows : List Eqn} (hlen : ∀ e ∈ rows, e.vars.length ≤ ℓA + ℓB) (hbel : ∀ e ∈ rows, e.Below (ℓA + ℓB)) (hΔ : rows.length * (ℓA + ℓB) ≤ Δ) {fA fB f₁ f₂ f₃ : ℕ → ZMod 2} (h : DecSat ℓA ℓB (ℓA + ℓB + Δ) (triangle (ℓA + ℓB) rows) fA fB f₁ f₂ f₃) (e : Eqn) : e ∈ rows → e.Holds (glue ℓA fA fB)

Every solution of the decoupled triangulated system comes from a solution of the original (cor:triang_and_decoupling_extend): its first two blocks, glued, solve the rows.

The canonical decider, decoupled

def MIPRE.Tailored.AnsRed.pureRows {X : Type u_1} [Fintype X] (G : TailoredGame X) (L : ℕ) (x y : X) (aR bR : Cost.BitStr) : List Eqn

The purified equations of a pair of questions, with the linear answers in tables of L entries.

Equations

• MIPRE.Tailored.AnsRed.pureRows G L x y aR bR = List.map (MIPRE.Tailored.AnsRed.pureEqn (G.lenR x) (G.lenL x) (G.lenR y) (G.lenL y) L aR bR) (G.cons x y aR bR)

theorem MIPRE.Tailored.AnsRed.pureRows_len {X : Type u_1} [Fintype X] (G : TailoredGame X) {L : ℕ} {x y : X} (hx : G.lenL x ≤ L) (hy : G.lenL y ≤ L) (aR bR : Cost.BitStr) (e : Eqn) : e ∈ pureRows G L x y aR bR → e.vars.length ≤ L + L

theorem MIPRE.Tailored.AnsRed.pureRows_below {X : Type u_1} [Fintype X] (G : TailoredGame X) {L : ℕ} {x y : X} (hx : G.lenL x ≤ L) (hy : G.lenL y ≤ L) (aR bR : Cost.BitStr) (e : Eqn) : e ∈ pureRows G L x y aR bR → e.Below (L + L)

theorem MIPRE.Tailored.AnsRed.decSat_of_accepts {X : Type u_1} [Fintype X] (G : TailoredGame X) {x y : X} {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) {L Δ : ℕ} (hx : G.lenL x ≤ L) (hy : G.lenL y ≤ L) (hacc : G.Accepts x y (aR ++ aL) (bR ++ bL)) : DecSat L L (L + L + Δ) (triangle (L + L) (pureRows G L x y aR bR)) (tbl L aL bL) (fun (j : ℕ) => tbl L aL bL (L + j)) (ext (L + L) (pureRows G L x y aR bR) (tbl L aL bL)) (ext (L + L) (pureRows G L x y aR bR) (tbl L aL bL)) (ext (L + L) (pureRows G L x y aR bR) (tbl L aL bL))

The canonical decider, triangulated and decoupled (claim:properties_of_L*, item 2, one direction): answers of the right lengths that the game accepts give the solution Extend of the table of their linear parts of the decoupled triangulated purified system, with Δ at least the number of constraints times 2L.

def MIPRE.Tailored.AnsRed.readBlock (k : ℕ) (f : ℕ → ZMod 2) : Cost.BitStr

The linear answer of length k read from a block.

Equations

• MIPRE.Tailored.AnsRed.readBlock k f = List.ofFn fun (j : Fin k) => MIPRE.LowDegree.BinaryLinear.bit (f ↑j)

@[simp]

theorem MIPRE.Tailored.AnsRed.length_readBlock (k : ℕ) (f : ℕ → ZMod 2) : List.length (readBlock k f) = k

theorem MIPRE.Tailored.AnsRed.bitAt_readBlock {k : ℕ} {f : ℕ → ZMod 2} {j : ℕ} (hj : j < k) : bitAt (readBlock k f) j = f j

theorem MIPRE.Tailored.AnsRed.accepts_of_decSat {X : Type u_1} [Fintype X] (G : TailoredGame X) {x y : X} {aR bR : Cost.BitStr} (haR : List.length aR = G.lenR x) (hbR : List.length bR = G.lenR y) {L Δ : ℕ} (hx : G.lenL x ≤ L) (hy : G.lenL y ≤ L) (hΔ : (G.cons x y aR bR).length * (L + L) ≤ Δ) {fA fB f₁ f₂ f₃ : ℕ → ZMod 2} (h : DecSat L L (L + L + Δ) (triangle (L + L) (pureRows G L x y aR bR)) fA fB f₁ f₂ f₃) : G.Accepts x y (aR ++ readBlock (G.lenL x) fA) (bR ++ readBlock (G.lenL y) fB)

The canonical decider from a solution of the decoupled system (claim:properties_of_L*, item 2, the other direction): if five assignments solve the decoupled triangulated purified system of the readable answers, with Δ at least the number of constraints times 2L, the game accepts the readable answers completed by the first two blocks, read at the linear lengths.