Passing a challenge of the associated test, under Checks 1–3

For an action σ passing Checks 1–3 (Checks g σ), the decision of the challenge at (x, y) of assocTest g reduces to Check 4: the point p passes exactly when every constraint word whose readable part is the readable value rdv σ x y p of p fixes p (passes_iff). The fixed literals then always hold (fixedLits_holds), and the readable literal of a readable variable holds for exactly one of its two words (inStab_readWord_iff).

Also: the value of the test as a μ-weighted average of pass probabilities (value_eq_sum), and the number of distinct constraint words (length_consWords_le').

Words as permutations

@[simp]

theorem MIPRE.Tailored.Sofic.wordPerm_nil {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) : σ.wordPerm [] = 1

@[simp]

theorem MIPRE.Tailored.Sofic.wordPerm_append {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (u v : SubgroupTestValue.Word) : σ.wordPerm (u ++ v) = σ.wordPerm u * σ.wordPerm v

@[simp]

theorem MIPRE.Tailored.Sofic.wordPerm_cons {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (l : SubgroupTestValue.Letter) (u : SubgroupTestValue.Word) : σ.wordPerm (l :: u) = σ.letterPerm l * σ.wordPerm u

theorem MIPRE.Tailored.Sofic.letterPerm_eq {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (k : ℕ) (b : Bool) : σ.letterPerm (k, b) = if b = true then (genPerm σ k)⁻¹ else genPerm σ k

@[simp]

theorem MIPRE.Tailored.Sofic.wordPerm_genW {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (k : ℕ) : σ.wordPerm (genW k) = genPerm σ k

theorem MIPRE.Tailored.Sofic.wordPerm_invW' {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (u : SubgroupTestValue.Word) : σ.wordPerm (invW u) = (σ.wordPerm u)⁻¹

theorem MIPRE.Tailored.Sofic.wordPerm_commW' {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (u v : SubgroupTestValue.Word) : σ.wordPerm (commW u v) = σ.wordPerm u * σ.wordPerm v * (σ.wordPerm u)⁻¹ * (σ.wordPerm v)⁻¹

theorem MIPRE.Tailored.Sofic.wordPerm_commW_of_commute {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) {u v : SubgroupTestValue.Word} (h : σ.wordPerm u * σ.wordPerm v = σ.wordPerm v * σ.wordPerm u) : σ.wordPerm (commW u v) = 1

The fixed and readable literals under Checks 1–3

@[simp]

theorem MIPRE.Tailored.Sofic.wordPerm_wJ {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} : σ.wordPerm wJ = genPerm σ genJ

@[simp]

theorem MIPRE.Tailored.Sofic.wordPerm_wX {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (x i : ℕ) : σ.wordPerm (wX g x i) = genPerm σ (genX g x i)

theorem MIPRE.Tailored.Sofic.mem_varsAt {g : TailoredGameValue.TailoredGameData} {x : ℕ} {X : SubgroupTestValue.Word} : X ∈ varsAt g x ↔ ∃ i < g.lenAt x, X = wX g x i

theorem MIPRE.Tailored.Sofic.fixedLits_holds {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) {x y : ℕ} (hx : x < g.nV + 1) (hy : y < g.nV + 1) (p : Fin σ.N) {wb : SubgroupTestValue.Word × Bool} (hwb : wb ∈ fixedLits g x y) : decide (σ.InStab p wb.1) = wb.2

The fixed literals hold (Checks 1 and 2).

theorem MIPRE.Tailored.Sofic.mem_readVars {g : TailoredGameValue.TailoredGameData} {x y : ℕ} {X : SubgroupTestValue.Word} (hX : X ∈ readVars g x y) : ∃ (z : ℕ) (i : ℕ), (z = x ∨ z = y) ∧ i < g.lenRAt z ∧ X = wX g z i

theorem MIPRE.Tailored.Sofic.length_readVars {g : TailoredGameValue.TailoredGameData} (x y : ℕ) : (readVars g x y).length = g.lenRAt x + g.lenRAt y

def MIPRE.Tailored.Sofic.rdv {g : TailoredGameValue.TailoredGameData} (σ : SubgroupTestValue.FiniteAction (nGen g)) (x y : ℕ) (p : Fin σ.N) : List Bool

The readable value of a point at (x, y): for each readable variable, whether it moves the point.

Equations

• MIPRE.Tailored.Sofic.rdv σ x y p = List.map (fun (X : SubgroupTestValue.Word) => decide ((σ.wordPerm X) p ≠ p)) (MIPRE.Tailored.Sofic.readVars g x y)

theorem MIPRE.Tailored.Sofic.length_rdv {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (x y : ℕ) (p : Fin σ.N) : (rdv σ x y p).length = g.lenRAt x + g.lenRAt y

theorem MIPRE.Tailored.Sofic.flatMap_pair_length {α : Type u_1} {β : Type u_2} (l : List α) (f h : α → β) : (List.flatMap (fun (a : α) => [f a, h a]) l).length = 2 * l.length

theorem MIPRE.Tailored.Sofic.flatMap_pair_getElem {α : Type u_1} {β : Type u_2} (l : List α) (f h : α → β) (t : ℕ) (b : Bool) (ht : t < l.length) (hlt : (2 * t + if b = true then 1 else 0) < (List.flatMap (fun (a : α) => [f a, h a]) l).length) : (List.flatMap (fun (a : α) => [f a, h a]) l)[2 * t + if b = true then 1 else 0] = if b = true then h l[t] else f l[t]

theorem MIPRE.Tailored.Sofic.length_readWords' {g : TailoredGameValue.TailoredGameData} (x y : ℕ) : (readWords g x y).length = 2 * (g.lenRAt x + g.lenRAt y)

theorem MIPRE.Tailored.Sofic.inStab_readWord_iff {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) {x y : ℕ} (hx : x < g.nV + 1) (hy : y < g.nV + 1) (p : Fin σ.N) (t : ℕ) (ht : t < (readVars g x y).length) (b : Bool) (hlt : (2 * t + if b = true then 1 else 0) < (readWords g x y).length) : σ.InStab p (readWords g x y)[2 * t + if b = true then 1 else 0] ↔ b = (rdv σ x y p)[t]

The readable literal of a readable variable holds for exactly one of its words: X when X fixes the point, J X when it moves it (Check 3).

The literals of the words K

theorem MIPRE.Tailored.Sofic.mem_allBits_iff {n : ℕ} {r : List Bool} : r ∈ allBits n ↔ r.length = n

theorem MIPRE.Tailored.Sofic.litHolds_fixed {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (x y : ℕ) (p : Fin σ.N) (i : ℕ) (hi : i < (fixedLits g x y).length) (b : Bool) : σ.LitHolds (words g x y) p (i, b) ↔ decide (σ.InStab p (fixedLits g x y)[i].1) = b

theorem MIPRE.Tailored.Sofic.litHolds_read {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (x y : ℕ) (p : Fin σ.N) (i : ℕ) (hi : i < (readWords g x y).length) (b : Bool) : σ.LitHolds (words g x y) p ((fixedLits g x y).length + i, b) ↔ decide (σ.InStab p (readWords g x y)[i]) = b

theorem MIPRE.Tailored.Sofic.litHolds_cons {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (x y : ℕ) (p : Fin σ.N) (i : ℕ) (hi : i < (consWords g x y).length) (b : Bool) : σ.LitHolds (words g x y) p ((fixedLits g x y).length + (readWords g x y).length + i, b) ↔ decide (σ.InStab p (consWords g x y)[i]) = b

theorem MIPRE.Tailored.Sofic.consWord_mem_consWords {g : TailoredGameValue.TailoredGameData} {x y : ℕ} {e : ℕ × ℕ × List Bool × List Bool} (he : e ∈ consAt g x y) : consWord g x y e.2.2.2 ∈ consWords g x y

theorem MIPRE.Tailored.Sofic.passes_iff {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) {x y : ℕ} (hx : x < g.nV + 1) (hy : y < g.nV + 1) (p : Fin σ.N) : σ.Passes (words g x y) (clauses g x y) p ↔ ∀ e ∈ consAt g x y, e.2.2.1 = rdv σ x y p → σ.InStab p (consWord g x y e.2.2.2)

Passing a challenge under Checks 1–3 is Check 4: every constraint word whose readable part is the point's readable value fixes the point.

The value of the test

theorem MIPRE.Tailored.Sofic.list_sum_map_range {M : Type u_1} [AddCommMonoid M] (n : ℕ) (f : ℕ → M) : (List.map f (List.range n)).sum = ∑ i : Fin n, f ↑i

theorem MIPRE.Tailored.Sofic.list_sum_map_flatMap {α : Type u_1} {β : Type u_2} {M : Type u_3} [AddCommMonoid M] (l : List α) (F : α → List β) (h : β → M) : (List.map h (List.flatMap F l)).sum = (List.map (fun (a : α) => (List.map h (F a)).sum) l).sum

theorem MIPRE.Tailored.Sofic.list_sum_map_square {β : Type u_1} {M : Type u_2} [AddCommMonoid M] (n : ℕ) (F : ℕ → ℕ → β) (h : β → M) : (List.map h (List.flatMap (fun (x : ℕ) => List.map (fun (y : ℕ) => F x y) (List.range n)) (List.range n))).sum = ∑ x : Fin n, ∑ y : Fin n, h (F ↑x ↑y)

theorem MIPRE.Tailored.Sofic.value_eq_sum {g : TailoredGameValue.TailoredGameData} (σ : SubgroupTestValue.FiniteAction (nGen g)) : (assocTest g).value σ = ∑ x : Fin (g.nV + 1), ∑ y : Fin (g.nV + 1), g.toGame.μ x y * σ.passProb (words g ↑x ↑y) (clauses g ↑x ↑y)

The value of the associated test is the μ-average of the pass probabilities of the challenges, μ being the game's question distribution.

Counting the constraint words

theorem MIPRE.Tailored.Sofic.length_consWords_le' {g : TailoredGameValue.TailoredGameData} (x y : ℕ) : (consWords g x y).length ≤ 2 ^ (g.lenAt x + g.lenAt y + 1) + 1

There are at most 2^{ℓ(x) + ℓ(y) + 1} + 1 distinct constraint words at (x, y).