theorem Hex.PermGroup.Orbit.mem_stabilizerGens {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (p : Perm n) : p ∈ stabilizerGens h ↔ ∃ (i : Fin S.size), ∃ (x : Fin c.points.size), schreier h S[↑i] ⋯ x = p

def Hex.PermGroup.Orbit.schreierWord {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (i : Fin S.size) (x : Fin c.points.size) : Program

A program for one recomputed Schreier element, in the same composition order as schreier. Orbit transporter programs retain their internal DAG references.

Equations

• Hex.PermGroup.Orbit.schreierWord h i x = c.words[↑(Hex.PermGroup.Orbit.act h S[↑i] ⋯ x)].inv.comp ((Hex.PermGroup.Generator.ofIndex S i false).program.comp c.words[↑x])

theorem Hex.PermGroup.Orbit.check_schreierWord {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (i : Fin S.size) (x : Fin c.points.size) : checkWord S (schreier h S[↑i] ⋯ x) (schreierWord h i x) = true

def Hex.PermGroup.Orbit.stabilizerWords {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) : Vector Program (stabilizerGens h).size

Provenance for every pair in stabilizerGens, in generator-major order.

Equations

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

theorem Hex.PermGroup.Orbit.check_stabilizerWords {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) : checkWords S (stabilizerGens h) (stabilizerWords h) = true

theorem Hex.PermGroup.Orbit.stabilizerGens_fixed {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) {base : Nat} (ha : ↑a = base) (hf : Chain.Fixed base S) : Chain.Fixed (base + 1) (stabilizerGens h)