Robustness: close actions have close values

Paper I, Claim I:1480: the value of a subgroup test changes by at most the significance-weighted Hamming distance between two actions on the same set. The significance of a generator k (I:1474) is the expected number of occurrences of k or k⁻¹ in the words of a challenge:

sig T k = E_{challenge} Σ_{w ∈ K} #{letters of w with generator k}.

The proof is the paper's. A word's permutation differs between the two actions at most at the points where one of its letters does (diffCard_mul, applied letter by letter), an inverse letter differing exactly as often as the direct one (diffCard_inv); the stabilizer decisions on the words of a challenge, hence the decision itself, agree wherever the words' permutations do; and a union bound over the words.

The paper states the claim for the edit distance, the minimum over relabellings; only the Hamming distance on one set is needed here.

def MIPRE.Tailored.Sofic.wordCount (k : ℕ) (w : SubgroupTestValue.Word) : ℕ

The number of letters of w whose generator is k, direct or inverse (v_k(w), I:1470; on an unreduced word, which can only increase the count).

Equations

• MIPRE.Tailored.Sofic.wordCount k w = List.countP (fun (l : SubgroupTestValue.Letter) => decide (l.1 = k)) w

noncomputable def MIPRE.Tailored.Sofic.sig (T : SubgroupTestValue.SubgroupTestData) (k : ℕ) : ℝ

The significance of the generator k in the test T (I:1474): the expected number of occurrences of k in the words of a challenge.

Equations

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

theorem MIPRE.Tailored.Sofic.sig_nonneg (T : SubgroupTestValue.SubgroupTestData) (k : ℕ) : 0 ≤ sig T k

List sums

Words

theorem MIPRE.Tailored.Sofic.FiniteActionLemmas.wordPerm_nil {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) : σ.wordPerm [] = 1

theorem MIPRE.Tailored.Sofic.FiniteActionLemmas.wordPerm_cons {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (l : SubgroupTestValue.Letter) (w : SubgroupTestValue.Word) : σ.wordPerm (l :: w) = σ.letterPerm l * σ.wordPerm w

theorem MIPRE.Tailored.Sofic.FiniteActionLemmas.wordPerm_append {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (u v : SubgroupTestValue.Word) : σ.wordPerm (u ++ v) = σ.wordPerm u * σ.wordPerm v

@[reducible, inline]

abbrev MIPRE.Tailored.Sofic.withPerms {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (ρ' : Fin n → Equiv.Perm (Fin σ.N)) : SubgroupTestValue.FiniteAction n

The action ρ' on the points of σ.

Equations

• MIPRE.Tailored.Sofic.withPerms σ ρ' = { N := σ.N, N_pos := ⋯, σ := ρ' }

theorem MIPRE.Tailored.Sofic.diffCard_letterPerm {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (ρ' : Fin n → Equiv.Perm (Fin σ.N)) (l : SubgroupTestValue.Letter) : diffCard (σ.letterPerm l) ((withPerms σ ρ').letterPerm l) = if h : l.1 < n then diffCard (σ.σ ⟨l.1, h⟩) (ρ' ⟨l.1, h⟩) else 0

theorem MIPRE.Tailored.Sofic.diffCard_wordPerm {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (ρ' : Fin n → Equiv.Perm (Fin σ.N)) (w : SubgroupTestValue.Word) : diffCard (σ.wordPerm w) ((withPerms σ ρ').wordPerm w) ≤ (List.map (fun (l : SubgroupTestValue.Letter) => diffCard (σ.letterPerm l) ((withPerms σ ρ').letterPerm l)) w).sum

theorem MIPRE.Tailored.Sofic.sum_letter_dist {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (ρ' : Fin n → Equiv.Perm (Fin σ.N)) (w : SubgroupTestValue.Word) : (List.map (fun (l : SubgroupTestValue.Letter) => ↑(diffCard (σ.letterPerm l) ((withPerms σ ρ').letterPerm l)) / ↑σ.N) w).sum = ∑ k : Fin n, ↑(wordCount (↑k) w) * dH (σ.σ k) (ρ' k)

The letters' distances, summed along a word, are the generators' distances weighted by their numbers of occurrences.

theorem MIPRE.Tailored.Sofic.passes_iff_of_agree {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (ρ' : Fin n → Equiv.Perm (Fin σ.N)) (K : List SubgroupTestValue.Word) (C : List (List (ℕ × Bool))) (p : Fin σ.N) (h : ∀ w ∈ K, (σ.wordPerm w) p = ((withPerms σ ρ').wordPerm w) p) : σ.Passes K C p ↔ (withPerms σ ρ').Passes K C p

The stabilizer decisions, hence the decision of a challenge, agree where the words' permutations do.

theorem MIPRE.Tailored.Sofic.abs_passProb_sub_le {n : ℕ} (σ : SubgroupTestValue.FiniteAction n) (ρ' : Fin n → Equiv.Perm (Fin σ.N)) (K : List SubgroupTestValue.Word) (C : List (List (ℕ × Bool))) : |σ.passProb K C - (withPerms σ ρ').passProb K C| ≤ (List.map (fun (w : SubgroupTestValue.Word) => ∑ k : Fin n, ↑(wordCount (↑k) w) * dH (σ.σ k) (ρ' k)) K).sum

theorem MIPRE.Tailored.Sofic.abs_value_sub_le (T : SubgroupTestValue.SubgroupTestData) (σ : SubgroupTestValue.FiniteAction T.nGen) (ρ' : Fin T.nGen → Equiv.Perm (Fin σ.N)) : |T.value σ - T.value (withPerms σ ρ')| ≤ ∑ k : Fin T.nGen, sig T ↑k * dH (σ.σ k) (ρ' k)

Robustness (Claim I:1480): two actions of the free group on the same finite set have test values within their significance-weighted Hamming distance.