Perturbing an action to pass Checks 1–3

The construction of Proposition I:2267, on an action τ of the associated test's generators that comes with a fixed-point-free involution s commuting with every letter (SwapData; the doubled action of MIPRE/Tailored/Sofic/Double.lean has one):

1. J₁ = invFix J₀, the involution near J₀ = τ(J) (Claim I:2561);
2. J₂, the fixed-point-free involution near J₁, sending the fixed points of J₁ along s (Claim I:2582);
3. at each vertex x, the variables X(x, i), i < ℓ(x), repaired by commFix with the central involution J₂ (Claims I:2600 and I:2643 together, and the readable repair of the paper's last step); the other generators are unchanged.

The result perturbed τ S passes Checks 1–3 at every point (checks_perturbed). The distances moved are bounded by the numbers of points at which the relations of Checks 1–3 fail (diffCard_J₂_le, diffCard_Xfix_le, card_bad_le), which the next file bounds by the probability of losing the test.

structure MIPRE.Tailored.Sofic.SwapData {n : ℕ} (τ : SubgroupTestValue.FiniteAction n) : Type

A fixed-point-free involution of the points of τ commuting with every letter.

• s : Equiv.Perm (Fin τ.N)
• invol (q : Fin τ.N) : self.s (self.s q) = q
• free (q : Fin τ.N) : self.s q ≠ q
• comm (l : SubgroupTestValue.Letter) (q : Fin τ.N) : (τ.letterPerm l) (self.s q) = self.s ((τ.letterPerm l) q)

def MIPRE.Tailored.Sofic.dblSwapData {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) : SwapData (double σ)

The swap of the doubled action.

Equations

• MIPRE.Tailored.Sofic.dblSwapData σ = { s := MIPRE.Tailored.Sofic.dblSwap σ, invol := ⋯, free := ⋯, comm := ⋯ }

@[reducible, inline]

abbrev MIPRE.Tailored.Sofic.J₀ {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) : Equiv.Perm (Fin τ.N)

J₀ = τ(J).

Equations

• MIPRE.Tailored.Sofic.J₀ τ = MIPRE.Tailored.Sofic.genPerm τ MIPRE.Tailored.Sofic.genJ

def MIPRE.Tailored.Sofic.J₁ {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) : Equiv.Perm (Fin τ.N)

Step 1: the involution J₁ near J₀.

Equations

• MIPRE.Tailored.Sofic.J₁ τ = MIPRE.Tailored.Sofic.invFix (MIPRE.Tailored.Sofic.J₀ τ)

theorem MIPRE.Tailored.Sofic.J₁_comm {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) (q : Fin τ.N) : (J₁ τ) (S.s q) = S.s ((J₁ τ) q)

def MIPRE.Tailored.Sofic.J₂ {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) : Equiv.Perm (Fin τ.N)

Step 2: the fixed-point-free involution J₂ near J₁.

Equations

• MIPRE.Tailored.Sofic.J₂ τ S = MIPRE.Tailored.Sofic.fpfFix (MIPRE.Tailored.Sofic.J₁ τ) S.s ⋯ ⋯ ⋯

theorem MIPRE.Tailored.Sofic.J₂_invol {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) (q : Fin τ.N) : (J₂ τ S) ((J₂ τ S) q) = q

theorem MIPRE.Tailored.Sofic.J₂_free {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) (q : Fin τ.N) : (J₂ τ S) q ≠ q

@[reducible, inline]

abbrev MIPRE.Tailored.Sofic.Xv (g : TailoredGameValue.TailoredGameData) (τ : SubgroupTestValue.FiniteAction (nGen g)) (x : ℕ) : ℕ → Equiv.Perm (Fin τ.N)

The variables at the vertex x.

Equations

• MIPRE.Tailored.Sofic.Xv g τ x i = MIPRE.Tailored.Sofic.genPerm τ (MIPRE.Tailored.Sofic.genX g x i)

noncomputable def MIPRE.Tailored.Sofic.Xfix {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) (x i : ℕ) : Equiv.Perm (Fin τ.N)

Step 3: the repaired variables at the vertex x.

Equations

• MIPRE.Tailored.Sofic.Xfix τ S x i = MIPRE.Tailored.Sofic.commFix (MIPRE.Tailored.Sofic.Xv g τ x) (g.lenAt x) (g.lenRAt x) (MIPRE.Tailored.Sofic.J₂ τ S) i

noncomputable def MIPRE.Tailored.Sofic.ρPert {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) (k : Fin (nGen g)) : Equiv.Perm (Fin τ.N)

The perturbed generators: J₂ for J, the repaired variables for the X(x, i), i < ℓ(x), and the other generators unchanged.

Equations

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

noncomputable def MIPRE.Tailored.Sofic.perturbed {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) : SubgroupTestValue.FiniteAction (nGen g)

The perturbed action.

Equations

• MIPRE.Tailored.Sofic.perturbed τ S = MIPRE.Tailored.Sofic.withPerms τ (MIPRE.Tailored.Sofic.ρPert τ S)

theorem MIPRE.Tailored.Sofic.genX_lt_nGen {g : TailoredGameValue.TailoredGameData} {x i : ℕ} (hx : x < g.nV + 1) (hi : i < g.ansLen) : genX g x i < nGen g

theorem MIPRE.Tailored.Sofic.genJ_lt_nGen {g : TailoredGameValue.TailoredGameData} : genJ < nGen g

theorem MIPRE.Tailored.Sofic.genPerm_eq {g : TailoredGameValue.TailoredGameData} (σ : SubgroupTestValue.FiniteAction (nGen g)) {k : ℕ} (hk : k < nGen g) : genPerm σ k = σ.σ ⟨k, hk⟩

theorem MIPRE.Tailored.Sofic.genX_decode {g : TailoredGameValue.TailoredGameData} {x i : ℕ} (hi : i < g.ansLen) : (genX g x i - 1) / g.ansLen = x ∧ (genX g x i - 1) % g.ansLen = i

theorem MIPRE.Tailored.Sofic.perturbed_J {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) : genPerm (perturbed τ S) genJ = J₂ τ S

theorem MIPRE.Tailored.Sofic.perturbed_X {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) {x i : ℕ} (hx : x < g.nV + 1) (hi : i < g.lenAt x) : genPerm (perturbed τ S) (genX g x i) = Xfix τ S x i

theorem MIPRE.Tailored.Sofic.perturbed_other {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) (k : Fin (nGen g)) (hk : ↑k ≠ genJ) (hx : ¬((↑k - 1) / g.ansLen < g.nV + 1 ∧ (↑k - 1) % g.ansLen < g.lenAt ((↑k - 1) / g.ansLen))) : ρPert τ S k = τ.σ k

theorem MIPRE.Tailored.Sofic.checks_perturbed {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) : Checks g (perturbed τ S)

The perturbed action passes Checks 1–3 (Proposition I:2267).

Distances

def MIPRE.Tailored.Sofic.fixJ {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) : ℕ

The number of fixed points of J₀.

Equations

• MIPRE.Tailored.Sofic.fixJ τ = {q : Fin τ.N | (MIPRE.Tailored.Sofic.J₀ τ) q = q}.card

def MIPRE.Tailored.Sofic.sqJ {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) : ℕ

The number of points J₀² moves.

Equations

• MIPRE.Tailored.Sofic.sqJ τ = {q : Fin τ.N | (MIPRE.Tailored.Sofic.J₀ τ) ((MIPRE.Tailored.Sofic.J₀ τ) q) ≠ q}.card

theorem MIPRE.Tailored.Sofic.diffCard_J₂_le {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) : diffCard (J₂ τ S) (J₀ τ) ≤ fixJ τ + 2 * sqJ τ

noncomputable def MIPRE.Tailored.Sofic.badX {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) (x : ℕ) : ℕ

The points at which the relations of Checks 1–3 at x fail for the variables and J₂.

Equations

• MIPRE.Tailored.Sofic.badX τ S x = {q : Fin τ.N | ¬MIPRE.Tailored.Sofic.LocGood (MIPRE.Tailored.Sofic.Xv g τ x) (g.lenAt x) (g.lenRAt x) (MIPRE.Tailored.Sofic.J₂ τ S) q}.card

theorem MIPRE.Tailored.Sofic.diffCard_Xfix_le {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) {x i : ℕ} (hi : i < g.lenAt x) : diffCard (Xfix τ S x i) (genPerm τ (genX g x i)) ≤ 2 ^ (g.lenAt x + 1) * badX τ S x

structure MIPRE.Tailored.Sofic.LocalBounds {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (x B : ℕ) : Prop

The relations at x, for J₀, each failing at no more than B points.

• comm (i : ℕ) : i < g.lenAt x → ∀ j < g.lenAt x, {q : Fin τ.N | (genPerm τ (genX g x i)) ((genPerm τ (genX g x j)) q) ≠ (genPerm τ (genX g x j)) ((genPerm τ (genX g x i)) q)}.card ≤ B
• sq (i : ℕ) : i < g.lenAt x → {q : Fin τ.N | (genPerm τ (genX g x i)) ((genPerm τ (genX g x i)) q) ≠ q}.card ≤ B
• J (i : ℕ) : i < g.lenAt x → {q : Fin τ.N | (J₀ τ) ((genPerm τ (genX g x i)) q) ≠ (genPerm τ (genX g x i)) ((J₀ τ) q)}.card ≤ B
• read (i : ℕ) : i < g.lenRAt x → {q : Fin τ.N | ¬((genPerm τ (genX g x i)) q = q ∨ (J₀ τ) ((genPerm τ (genX g x i)) q) = q)}.card ≤ B

theorem MIPRE.Tailored.Sofic.localBounds_left {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (x y : ℕ) : LocalBounds τ x (npass τ g x y)

The challenges at (x, y) and (y, x) bound the relations at x.

theorem MIPRE.Tailored.Sofic.localBounds_right {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (x y : ℕ) : LocalBounds τ x (npass τ g y x)

theorem MIPRE.Tailored.Sofic.card_bad_le {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) {x B : ℕ} (hB : LocalBounds τ x B) : badX τ S x ≤ (g.lenAt x ^ 2 + 3 * g.lenAt x) * B + 3 * g.lenAt x * diffCard (J₂ τ S) (J₀ τ)

The bad points at x number at most (ℓ² + 3ℓ) B + 3ℓ d(J₂, J₀).