The value of the associated test, challenge by challenge

For the associated test assocTest g of MIPRE/Tailored/Sofic/Assoc.lean:

• qw g x y, the weight of the challenge at the question pair (x, y) (the game's convention when every weight vanishes: weight 1 at (0, 0)), and qwTot g > 0 their total; every sum over the challenges is the qw-weighted sum over the pairs (x, y), x, y ≤ nV (sum_challenges), so the value and the significance are such sums (value_eq, sig_eq).
• The per-point consequences of passing the challenge at (x, y) (Checks 1–3, I:2086): J moves the point, J², [J, X], X², [X, X'] fix it for the variables X, X' at x and at y, and each readable variable X fixes it or J X does. Hence the number of points where one of these fails is at most the number of points failing the challenge (card_J_fixed_le and the following).

Weights

def MIPRE.Tailored.Sofic.qw (g : TailoredGameValue.TailoredGameData) (x y : ℕ) : ℕ

The weight of the challenge at (x, y).

Equations

• MIPRE.Tailored.Sofic.qw g x y = if (MIPRE.Tailored.Sofic.wts g).totalWeight = 0 then if x = 0 ∧ y = 0 then 1 else 0 else (MIPRE.Tailored.Sofic.wts g).questionWeight x y

def MIPRE.Tailored.Sofic.qwTot (g : TailoredGameValue.TailoredGameData) : ℕ

The total weight of the challenges.

Equations

• MIPRE.Tailored.Sofic.qwTot g = ∑ x ∈ Finset.range (g.nV + 1), ∑ y ∈ Finset.range (g.nV + 1), MIPRE.Tailored.Sofic.qw g x y

theorem MIPRE.Tailored.Sofic.qwTot_eq_of_ne (g : TailoredGameValue.TailoredGameData) (h : (wts g).totalWeight ≠ 0) : qwTot g = (wts g).totalWeight

theorem MIPRE.Tailored.Sofic.qwTot_pos (g : TailoredGameValue.TailoredGameData) : 0 < qwTot g

theorem MIPRE.Tailored.Sofic.sum_challenges (g : TailoredGameValue.TailoredGameData) (Ψ : List SubgroupTestValue.Word × List (List (ℕ × Bool)) → ℝ) : (List.map (fun (c : ℕ × List SubgroupTestValue.Word × List (List (ℕ × Bool))) => ↑c.1 * Ψ c.2) (assocTest g).challenges).sum = ∑ x ∈ Finset.range (g.nV + 1), ∑ y ∈ Finset.range (g.nV + 1), ↑(qw g x y) * Ψ (words g x y, clauses g x y)

Every weighted sum over the challenges is the qw-weighted sum over the question pairs.

theorem MIPRE.Tailored.Sofic.assocTest_totalWeight_eq (g : TailoredGameValue.TailoredGameData) : ↑(assocTest g).totalWeight = ↑(qwTot g)

theorem MIPRE.Tailored.Sofic.value_eq (g : TailoredGameValue.TailoredGameData) (σ : SubgroupTestValue.FiniteAction (nGen g)) : (assocTest g).value σ = (∑ x ∈ Finset.range (g.nV + 1), ∑ y ∈ Finset.range (g.nV + 1), ↑(qw g x y) * σ.passProb (words g x y) (clauses g x y)) / ↑(qwTot g)

The value of the associated test as a sum over the question pairs.

theorem MIPRE.Tailored.Sofic.sig_eq (g : TailoredGameValue.TailoredGameData) (k : ℕ) : sig (assocTest g) k = (∑ x ∈ Finset.range (g.nV + 1), ∑ y ∈ Finset.range (g.nV + 1), ↑(qw g x y) * (List.map (fun (w : SubgroupTestValue.Word) => ↑(wordCount k w)) (words g x y)).sum) / ↑(qwTot g)

The significance in the associated test as a sum over the question pairs.

Words and their permutations

theorem MIPRE.Tailored.Sofic.letterPerm_flip {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (l : SubgroupTestValue.Letter) : σ.letterPerm (l.1, !l.2) = (σ.letterPerm l)⁻¹

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_genW {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (k : ℕ) : σ.wordPerm (genW k) = genPerm σ k

Passing a challenge

theorem MIPRE.Tailored.Sofic.fixed_of_passes {g : TailoredGameValue.TailoredGameData} {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) {x y : ℕ} {q : Fin σ.N} (h : σ.Passes (words g x y) (clauses g x y) q) {wb : SubgroupTestValue.Word × Bool} (hwb : wb ∈ fixedLits g x y) : decide (σ.InStab q wb.1) = wb.2

Passing a challenge gives every fixed literal (Checks 1 and 2).

theorem MIPRE.Tailored.Sofic.read_of_passes {g : TailoredGameValue.TailoredGameData} {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) {x y : ℕ} {q : Fin σ.N} (h : σ.Passes (words g x y) (clauses g x y) q) {X : SubgroupTestValue.Word} (hX : X ∈ readVars g x y) : σ.InStab q X ∨ σ.InStab q (wJ ++ X)

Passing a challenge gives every readable literal (Check 3).