The doubled action

The disjoint union σ ⊕ σ of a finite action with itself, on Fin 2 × Fin N ≃ Fin (2N). Every stabilizer occurs twice as often on twice as many points, so every challenge is passed with the same probability and the value is unchanged (value_double). The swap of the two copies is a fixed-point-free involution commuting with every letter (dblSwap).

This replaces the paper's padding of an odd set by one point (Claim I:2582 and the proof of Proposition I:2267): on the doubled set, the fixed points of an involution commuting with the swap can be sent along the swap, and every distance is measured on a single point set.

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

The disjoint union of σ with itself.

Equations

• MIPRE.Tailored.Sofic.double σ = { N := 2 * σ.N, N_pos := ⋯, σ := fun (k : Fin n) => finProdFinEquiv.permCongr ((Equiv.refl (Fin 2)).prodCongr (σ.σ k)) }

theorem MIPRE.Tailored.Sofic.double_N {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) : (double σ).N = 2 * σ.N

def MIPRE.Tailored.Sofic.dblE {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) : Fin 2 × Fin σ.N ≃ Fin (double σ).N

The two copies of the points of σ, as the points of double σ.

Equations

• MIPRE.Tailored.Sofic.dblE σ = finProdFinEquiv

theorem MIPRE.Tailored.Sofic.double_σ_apply {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (k : Fin n) (i : Fin 2) (p : Fin σ.N) : ((double σ).σ k) ((dblE σ) (i, p)) = (dblE σ) (i, (σ.σ k) p)

theorem MIPRE.Tailored.Sofic.double_σ_inv_apply {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (k : Fin n) (i : Fin 2) (p : Fin σ.N) : ((double σ).σ k)⁻¹ ((dblE σ) (i, p)) = (dblE σ) (i, (σ.σ k)⁻¹ p)

theorem MIPRE.Tailored.Sofic.double_letterPerm {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (l : SubgroupTestValue.Letter) (i : Fin 2) (p : Fin σ.N) : ((double σ).letterPerm l) ((dblE σ) (i, p)) = (dblE σ) (i, (σ.letterPerm l) p)

theorem MIPRE.Tailored.Sofic.double_wordPerm {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (w : SubgroupTestValue.Word) (i : Fin 2) (p : Fin σ.N) : ((double σ).wordPerm w) ((dblE σ) (i, p)) = (dblE σ) (i, (σ.wordPerm w) p)

theorem MIPRE.Tailored.Sofic.double_inStab {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (w : SubgroupTestValue.Word) (i : Fin 2) (p : Fin σ.N) : (double σ).InStab ((dblE σ) (i, p)) w ↔ σ.InStab p w

theorem MIPRE.Tailored.Sofic.double_passes {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (K : List SubgroupTestValue.Word) (C : List (List (ℕ × Bool))) (i : Fin 2) (p : Fin σ.N) : (double σ).Passes K C ((dblE σ) (i, p)) ↔ σ.Passes K C p

theorem MIPRE.Tailored.Sofic.double_passProb {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (K : List SubgroupTestValue.Word) (C : List (List (ℕ × Bool))) : (double σ).passProb K C = σ.passProb K C

theorem MIPRE.Tailored.Sofic.value_double (T : SubgroupTestValue.SubgroupTestData) (σ : SubgroupTestValue.FiniteAction T.nGen) : T.value (double σ) = T.value σ

Doubling does not change the value.

def MIPRE.Tailored.Sofic.dblSwap {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) : Equiv.Perm (Fin (double σ).N)

The swap of the two copies.

Equations

• MIPRE.Tailored.Sofic.dblSwap σ = (MIPRE.Tailored.Sofic.dblE σ).permCongr (Equiv.prodCongr (Equiv.swap 0 1) (Equiv.refl (Fin σ.N)))

theorem MIPRE.Tailored.Sofic.dblSwap_apply {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (i : Fin 2) (p : Fin σ.N) : (dblSwap σ) ((dblE σ) (i, p)) = (dblE σ) ((Equiv.swap 0 1) i, p)

theorem MIPRE.Tailored.Sofic.dblSwap_invol {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (q : Fin (double σ).N) : (dblSwap σ) ((dblSwap σ) q) = q

theorem MIPRE.Tailored.Sofic.dblSwap_free {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (q : Fin (double σ).N) : (dblSwap σ) q ≠ q

theorem MIPRE.Tailored.Sofic.dblSwap_comm {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (l : SubgroupTestValue.Letter) (q : Fin (double σ).N) : ((double σ).letterPerm l) ((dblSwap σ) q) = (dblSwap σ) (((double σ).letterPerm l) q)