@[reducible, inline]

abbrev Hex.PermGroup.Action.Step {n : Nat} (G : Group n) : Type

A signed reference to an original input generator.

Equations

• Hex.PermGroup.Action.Step G = (Fin G.generators.size × Bool)

def Hex.PermGroup.Action.Step.element {n : Nat} {G : Group n} (s : Step G) : Element G

Equations

• s.element = if s.snd = true then Hex.PermGroup.Element.inv ⟨G.generators[↑s.fst], ⋯⟩ else ⟨G.generators[↑s.fst], ⋯⟩

def Hex.PermGroup.Action.Step.all {n : Nat} (G : Group n) : List (Step G)

Equations

• Hex.PermGroup.Action.Step.all G = List.flatMap (fun (i : Fin G.generators.size) => [(i, false), (i, true)]) (List.finRange G.generators.size)

@[simp]

theorem Hex.PermGroup.Action.Step.mem_all {n : Nat} {G : Group n} (s : Step G) : s ∈ all G

def Hex.PermGroup.Action.Step.advance {n : Nat} {G : Group n} (s : Step G) (b : Program.Builder G.generators) (r : Fin b.values.size) : Program.Builder G.generators

Append a signed generator and its left product with an earlier root.

Equations

• s.advance b r = if s.snd = true then let g := b.generator s.fst; let v := g.inv ⟨b.values.size, ⋯⟩; v.comp ⟨b.values.size + 1, ⋯⟩ ⟨↑r, ⋯⟩ else b.act s.fst r

theorem Hex.PermGroup.Action.Step.advance_size {n : Nat} {G : Group n} (s : Step G) (b : Program.Builder G.generators) (r : Fin b.values.size) : (s.advance b r).values.size = b.values.size + if s.snd = true then 3 else 2

theorem Hex.PermGroup.Action.Step.advance_le {n : Nat} {G : Group n} (s : Step G) (b : Program.Builder G.generators) (r : Fin b.values.size) : b.values.size ≤ (s.advance b r).values.size

theorem Hex.PermGroup.Action.Step.advance_pos {n : Nat} {G : Group n} (s : Step G) (b : Program.Builder G.generators) (r : Fin b.values.size) : 0 < (s.advance b r).values.size

theorem Hex.PermGroup.Action.Step.advance_get {n : Nat} {G : Group n} (s : Step G) (b : Program.Builder G.generators) (r i : Fin b.values.size) : (s.advance b r).values[↑i] = b.values[↑i]

theorem Hex.PermGroup.Action.Step.advance_last {n : Nat} {G : Group n} (s : Step G) (b : Program.Builder G.generators) (r : Fin b.values.size) : (s.advance b r).values[(s.advance b r).values.size - 1] = s.element.comp b.values[↑r]

The appended root denotes precisely the edge permutation times its parent.