Soundness of the associated test (Proposition I:2279)

An action σ passing Checks 1–3 of assocTest g everywhere gives the Z-aligned permutation strategy quotStrat σ hσ, whose rejection probability at each question pair (x, y) is at most 2 |consWords x y| times the probability that σ fails the challenge at (x, y) (rej_quotStrat_le). With at most 2^{2(Λ+1)} distinct constraint words, this gives (gameValue_ge_of_checks)

1 - Cq · 2^{2(Λ+1)} · (1 - val(T̃, σ)) ≤ val(G), Cq = 2.

The proof, for each distinct constraint word w at (x, y):

• a rejected answer pair with nonzero weight violates some constraint, whose word is one of the w (rej_le_sum_viol): malformed answers have zero projection, unequal answers at a loop orthogonal ones;
• the probability of violating a constraint with word w is (1/m) ∑_{j ∈ R_w} Re ((1 - M_w)/2)_{jj}, R_w the basis points whose readable signs are the readable value of such a constraint (sum_viol_eq, from the trace identity); all constraints with the word w have the same matrix M_w, the induced signed permutation of w, so the violated ones are those of sign -1;
• ((1 - M_w)/2)_{jj} vanishes when w fixes the representative j, and the representatives of R_w that w moves fail the challenge (passes_iff).

def MIPRE.Tailored.Sofic.Cq : ℝ

The constant of Proposition I:2279.

Equations

• MIPRE.Tailored.Sofic.Cq = 2

def MIPRE.Tailored.Sofic.ViolW (g : TailoredGameValue.TailoredGameData) (x y : Fin (g.nV + 1)) (w : SubgroupTestValue.Word) (a b : Fin g.ansLen → Bool) : Prop

The answer pair (a, b) violates a constraint at (x, y) whose word is w.

Equations

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

def MIPRE.Tailored.Sofic.ReadW (g : TailoredGameValue.TailoredGameData) (x y : Fin (g.nV + 1)) (w : SubgroupTestValue.Word) (r : List Bool) : Prop

The readable value r carries a constraint at (x, y) whose word is w.

Equations

• MIPRE.Tailored.Sofic.ReadW g x y w r = ∃ e ∈ MIPRE.Tailored.Sofic.consAt g ↑x ↑y, MIPRE.Tailored.Sofic.consWord g (↑x) (↑y) e.2.2.2 = w ∧ e.2.2.1 = r

theorem MIPRE.Tailored.Sofic.mem_consAt {g : TailoredGameValue.TailoredGameData} {x y : ℕ} {e : ℕ × ℕ × List Bool × List Bool} : e ∈ consAt g x y ↔ e ∈ g.cons ∧ e.1 = x ∧ e.2.1 = y

theorem MIPRE.Tailored.Sofic.ZStrat.rej_le_sum_viol {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) : S.rej x y ≤ ∑ w ∈ (consWords g ↑x ↑y).toFinset, ∑ a : Fin g.ansLen → Bool, ∑ b : Fin g.ansLen → Bool, if ViolW g x y w a b then (S.proj x a * S.proj y b).trace.re / ↑S.m else 0

A rejected answer pair violates a constraint (union bound over the distinct words).

theorem MIPRE.Tailored.Sofic.ZStrat.sum_viol_eq {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) (w : SubgroupTestValue.Word) (M : Matrix (Fin S.m) (Fin S.m) ℂ) (hM : ∀ e ∈ consAt g ↑x ↑y, consWord g (↑x) (↑y) e.2.2.2 = w → S.consMat x y e.2.2.2 = M) : (∑ a : Fin g.ansLen → Bool, ∑ b : Fin g.ansLen → Bool, if ViolW g x y w a b then (S.proj x a * S.proj y b).trace.re / ↑S.m else 0) = (∑ j : Fin S.m, if ReadW g x y w (S.rsgn x j ++ S.rsgn y j) then 1 / 2 * (1 - M j j) else 0).re / ↑S.m

The probability of violating a constraint with word w, by the trace identity, for a matrix M that is the matrix of every constraint with word w.

The quotient strategy

theorem MIPRE.Tailored.Sofic.unat_quotStrat {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) (z : Fin (g.nV + 1)) (i : ℕ) (hi : i < g.lenAt ↑z) : (quotStrat σ hσ).Unat z i = (indF σ (genPerm σ (genX g (↑z) i))).toMatrix

theorem MIPRE.Tailored.Sofic.consMat_quotStrat {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) (x y : Fin (g.nV + 1)) (c : List Bool) : (quotStrat σ hσ).consMat x y c = (wordSP (fun (k : ℕ) => indF σ (genPerm σ k)) (consWord g (↑x) (↑y) c)).toMatrix

theorem MIPRE.Tailored.Sofic.mem_consWord {g : TailoredGameValue.TailoredGameData} {x y : Fin (g.nV + 1)} {c : List Bool} {l : SubgroupTestValue.Letter} (hl : l ∈ consWord g (↑x) (↑y) c) : l = (genJ, false) ∨ ∃ (z : Fin (g.nV + 1)), ∃ i < g.lenAt ↑z, l = (genX g (↑z) i, false)

theorem MIPRE.Tailored.Sofic.indF_wordPerm {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) (w : SubgroupTestValue.Word) (hw : ∀ l ∈ w, l.2 = false ∧ CommJ (genPerm σ genJ) (genPerm σ l.1)) : CommJ (genPerm σ genJ) (σ.wordPerm w) ∧ indF σ (σ.wordPerm w) = wordSP (fun (k : ℕ) => indF σ (genPerm σ k)) w

theorem MIPRE.Tailored.Sofic.consWord_indF {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) (x y : Fin (g.nV + 1)) (c : List Bool) : CommJ (genPerm σ genJ) (σ.wordPerm (consWord g (↑x) (↑y) c)) ∧ (quotStrat σ hσ).consMat x y c = (indF σ (σ.wordPerm (consWord g (↑x) (↑y) c))).toMatrix

theorem MIPRE.Tailored.Sofic.rbit_quotStrat {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) (x : Fin (g.nV + 1)) (i : ℕ) (hi : i < g.lenRAt ↑x) (j : Fin (quotStrat σ hσ).m) : (quotStrat σ hσ).rbit x i j = decide ((genPerm σ (genX g (↑x) i)) (repPt σ j) ≠ repPt σ j)

theorem MIPRE.Tailored.Sofic.rsgn_quotStrat {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) (x y : Fin (g.nV + 1)) (j : Fin (quotStrat σ hσ).m) : (quotStrat σ hσ).rsgn x j ++ (quotStrat σ hσ).rsgn y j = rdv σ (↑x) (↑y) (repPt σ j)

theorem MIPRE.Tailored.Sofic.one_sub_passProb {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) : 1 - σ.passProb K cl = ↑{p : Fin σ.N | ¬σ.Passes K cl p}.card / ↑σ.N

The failure probability of a challenge.

theorem MIPRE.Tailored.Sofic.rej_quotStrat_le {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) (x y : Fin (g.nV + 1)) : (quotStrat σ hσ).rej x y ≤ 2 * ↑(consWords g ↑x ↑y).length * (1 - σ.passProb (words g ↑x ↑y) (clauses g ↑x ↑y))

The rejection probability of the quotient strategy at a question pair is at most 2 |consWords| times the failure probability of the challenge.

Proposition I:2279

theorem MIPRE.Tailored.Sofic.length_consWords_le_pow {g : TailoredGameValue.TailoredGameData} (x y : Fin (g.nV + 1)) : ↑(consWords g ↑x ↑y).length ≤ 2 ^ (2 * (g.ansLen + 1))

theorem MIPRE.Tailored.Sofic.passProb_le_one {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (K : List SubgroupTestValue.Word) (cl : List (List (ℕ × Bool))) : σ.passProb K cl ≤ 1

theorem MIPRE.Tailored.Sofic.gameValue_ge_of_checks (g : TailoredGameValue.TailoredGameData) (σ : SubgroupTestValue.FiniteAction (nGen g)) (hσ : Checks g σ) : 1 - Cq * 2 ^ (2 * (g.ansLen + 1)) * (1 - (assocTest g).value σ) ≤ HaltingGameValue.gameValue g.toGame

Soundness half of Proposition I:2279: an action passing Checks 1–3 everywhere loses the game at most Cq · 2^{2(Λ+1)} times as often as it loses the test.