Documentation

MIPRE.Tailored.Sofic.Local

Checks 1–3 fail only where a challenge fails #

For a finite action σ and a question pair (x, y), npass σ x y is the number of points whose stabilizer fails the challenge at (x, y). Each relation of Checks 1–3 among J and the variables at x and at y (I:2086) fails at no more points than that: J fixes a point, J² moves it, J and X do not commute at it, X² moves it, two variables at one vertex do not commute at it, or a readable variable X moves it while J X moves it too.

source
def MIPRE.Tailored.Sofic.npass {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (g : TailoredGameValue.TailoredGameData) (x y : ℕ) :
ℕ

The number of points failing the challenge at (x, y).

Equations
Instances For
    source
    theorem MIPRE.Tailored.Sofic.card_J_fixed_le {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (g : TailoredGameValue.TailoredGameData) (x y : ℕ) :
    {q : Fin σ.N | (genPerm σ genJ) q = q}.card ≤ npass σ g x y
    source
    theorem MIPRE.Tailored.Sofic.card_J_sq_le {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (g : TailoredGameValue.TailoredGameData) (x y : ℕ) :
    {q : Fin σ.N | (genPerm σ genJ) ((genPerm σ genJ) q) ≠ q}.card ≤ npass σ g x y
    source
    theorem MIPRE.Tailored.Sofic.card_JX_le {g : TailoredGameValue.TailoredGameData} {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) {x y z i : ℕ} (hz : z = x ∨ z = y) (hi : i < g.lenAt z) :
    {q : Fin σ.N | (genPerm σ genJ) ((genPerm σ (genX g z i)) q) ≠ (genPerm σ (genX g z i)) ((genPerm σ genJ) q)}.card ≤ npass σ g x y
    source
    theorem MIPRE.Tailored.Sofic.card_X_sq_le {g : TailoredGameValue.TailoredGameData} {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) {x y z i : ℕ} (hz : z = x ∨ z = y) (hi : i < g.lenAt z) :
    {q : Fin σ.N | (genPerm σ (genX g z i)) ((genPerm σ (genX g z i)) q) ≠ q}.card ≤ npass σ g x y
    source
    theorem MIPRE.Tailored.Sofic.card_XX_le {g : TailoredGameValue.TailoredGameData} {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) {x y z i j : ℕ} (hz : z = x ∨ z = y) (hi : i < g.lenAt z) (hj : j < g.lenAt z) :
    {q : Fin σ.N | (genPerm σ (genX g z i)) ((genPerm σ (genX g z j)) q) ≠ (genPerm σ (genX g z j)) ((genPerm σ (genX g z i)) q)}.card ≤ npass σ g x y
    source
    theorem MIPRE.Tailored.Sofic.card_read_le {g : TailoredGameValue.TailoredGameData} {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) {x y z i : ℕ} (hz : z = x ∨ z = y) (hi : i < g.lenRAt z) :
    {q : Fin σ.N | ¬((genPerm σ (genX g z i)) q = q ∨ (genPerm σ genJ) ((genPerm σ (genX g z i)) q) = q)}.card ≤ npass σ g x y