The signed permutation of a constraint word

Given a signed permutation γ k for each generator k, a word w has the signed permutation wordSP γ w, the product of its letters. When γ J = -1 and γ X(z, i) has matrix U z i, the matrix of the constraint word of c is consMat c = (-1)^{c_J} U^α V^β (toMatrix_wordSP_consWord): the word is J^{c_J} ∏ X(x, i)^{c_i} ∏ X(y, i)^{c_{ℓ(x)+i}} and U^α is the same product over Fin Λ, the coefficients beyond ℓ(x) being zero.

The diagonal entries of a signed permutation matrix are 1 at the points it fixes with sign +, and otherwise -1 or 0 (toMatrix_apply_self_eq_one_iff, re_one_sub_toMatrix_apply_self).

Signed permutations of words

def MIPRE.Tailored.Sofic.wordSP {Ω : Type u_1} (γ : ℕ → SignedPerm Ω) (w : SubgroupTestValue.Word) : SignedPerm Ω

The signed permutation of a word, the product of its letters, a letter (k, b) acting as γ k, inverted when b.

Equations

• MIPRE.Tailored.Sofic.wordSP γ w = (List.map (fun (l : SubgroupTestValue.Letter) => if l.2 = true then (γ l.1)⁻¹ else γ l.1) w).prod

@[simp]

theorem MIPRE.Tailored.Sofic.wordSP_nil {Ω : Type u_1} (γ : ℕ → SignedPerm Ω) : wordSP γ [] = 1

@[simp]

theorem MIPRE.Tailored.Sofic.wordSP_append {Ω : Type u_1} (γ : ℕ → SignedPerm Ω) (u v : SubgroupTestValue.Word) : wordSP γ (u ++ v) = wordSP γ u * wordSP γ v

@[simp]

theorem MIPRE.Tailored.Sofic.wordSP_genW {Ω : Type u_1} (γ : ℕ → SignedPerm Ω) (k : ℕ) : wordSP γ (genW k) = γ k

@[simp]

theorem MIPRE.Tailored.Sofic.wordSP_wJ {Ω : Type u_1} (γ : ℕ → SignedPerm Ω) : wordSP γ wJ = γ genJ

theorem MIPRE.Tailored.Sofic.wordSP_flatMap_genW {Ω : Type u_1} (γ : ℕ → SignedPerm Ω) (l : List ℕ) (f : ℕ → ℕ) : wordSP γ (List.flatMap (fun (i : ℕ) => genW (f i)) l) = (List.map (fun (i : ℕ) => γ (f i)) l).prod

theorem MIPRE.Tailored.Sofic.toMatrix_apply_self {Ω : Type u_1} [DecidableEq Ω] (s : SignedPerm Ω) (j : Ω) : s.toMatrix j j = if s.perm j = j then bitSign (s.sign j) else 0

theorem MIPRE.Tailored.Sofic.toMatrix_apply_self_eq_one_iff {Ω : Type u_1} [DecidableEq Ω] (s : SignedPerm Ω) (j : Ω) : s.toMatrix j j = 1 ↔ s.perm j = j ∧ s.sign j = false

theorem MIPRE.Tailored.Sofic.re_one_sub_toMatrix_apply_self_le {Ω : Type u_1} [DecidableEq Ω] (s : SignedPerm Ω) (j : Ω) : (1 / 2 * (1 - s.toMatrix j j)).re ≤ if s.perm j = j ∧ s.sign j = false then 0 else 1

Re (1 - M_{jj}) / 2 is 0 where the signed permutation fixes j with sign +, and at most 1 elsewhere.

theorem MIPRE.Tailored.Sofic.re_one_sub_toMatrix_apply_self_nonneg {Ω : Type u_1} [DecidableEq Ω] (s : SignedPerm Ω) (j : Ω) : 0 ≤ (1 / 2 * (1 - s.toMatrix j j)).re

The matrix of a constraint word

theorem MIPRE.Tailored.Sofic.list_prod_map_filter {M : Type u_1} [Monoid M] (l : List ℕ) (p : ℕ → Bool) (f : ℕ → M) : (List.map f (List.filter p l)).prod = (List.map (fun (i : ℕ) => if p i = true then f i else 1) l).prod

A product over the filtered indices, as a product of ites.

noncomputable def MIPRE.Tailored.Sofic.ZStrat.Unat {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (z : Fin (g.nV + 1)) (i : ℕ) : Matrix (Fin S.m) (Fin S.m) ℂ

The observable U z i, for a natural i, the identity beyond Λ.

Equations

• S.Unat z i = if h : i < g.ansLen then S.U z ⟨i, h⟩ else 1

theorem MIPRE.Tailored.Sofic.ZStrat.obsChar_eq_prod {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (z : Fin (g.nV + 1)) (ℓ : ℕ) (hℓ : ℓ ≤ g.ansLen) (q : ℕ → Bool) : (obsChar (S.U z) fun (i : Fin g.ansLen) => decide (↑i < ℓ) && q ↑i) = (List.map (S.Unat z) (List.filter q (List.range ℓ))).prod

U^α, for α supported on the first ℓ coordinates, as a product over range ℓ.

theorem MIPRE.Tailored.Sofic.ZStrat.obsChar_coefX {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x : Fin (g.nV + 1)) (c : List Bool) : obsChar (S.U x) (coefX g x c) = (List.map (S.Unat x) (List.filter (fun (i : ℕ) => c.getD i false) (List.range (g.lenAt ↑x)))).prod

theorem MIPRE.Tailored.Sofic.ZStrat.obsChar_coefY {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) (c : List Bool) : obsChar (S.U y) (coefY g x y c) = (List.map (S.Unat y) (List.filter (fun (i : ℕ) => c.getD (g.lenAt ↑x + i) false) (List.range (g.lenAt ↑y)))).prod

theorem MIPRE.Tailored.Sofic.ZStrat.toMatrix_wordSP_consWord {g : TailoredGameValue.TailoredGameData} (S : ZStrat g) (x y : Fin (g.nV + 1)) (γ : ℕ → SignedPerm (Fin S.m)) (hJ : (γ genJ).toMatrix = -1) (hX : ∀ (z : Fin (g.nV + 1)), ∀ i < g.lenAt ↑z, (γ (genX g (↑z) i)).toMatrix = S.Unat z i) (c : List Bool) : (wordSP γ (consWord g (↑x) (↑y) c)).toMatrix = S.consMat x y c

The matrix of a constraint word is the constraint's matrix, for generators whose signed permutations have matrices -1 (for J) and the observables (for the variables).