theorem Hex.PermGroup.Chain.before_irrefl {n : Nat} (p : Perm n) : ¬before p p

theorem Hex.PermGroup.Chain.before_trans {n : Nat} {p q r : Perm n} (hpq : before p q) (hqr : before q r) : before p r

structure Hex.PermGroup.Generator {n : Nat} (S : Array (Perm n)) : Type

A working generator with its signed input reference. Its permutation is cached, so sorting never recomputes inverses.

• value : Perm n
• source : Fin S.size × Bool
• valid : self.value = Word.letter S self.source

def Hex.PermGroup.Generator.ofIndex {n : Nat} (S : Array (Perm n)) (i : Fin S.size) (inverse : Bool) : Generator S

Equations

• Hex.PermGroup.Generator.ofIndex S i inverse = { value := Hex.PermGroup.Word.letter S (i, inverse), source := (i, inverse), valid := ⋯ }

def Hex.PermGroup.Generator.images {n : Nat} (p : Perm n) : List Nat

Equations

• Hex.PermGroup.Generator.images p = List.map Fin.val p.vec.toList

theorem Hex.PermGroup.Generator.images_injective {n : Nat} {p q : Perm n} (h : images p = images q) : p = q

def Hex.PermGroup.Generator.le {n : Nat} {S : Array (Perm n)} (x y : Generator S) : Bool

The non-strict ordering used by merge sort; the checker retains its separate strict comparison on image arrays.

Equations

• x.le y = (compare (Hex.PermGroup.Generator.images x.value) (Hex.PermGroup.Generator.images y.value)).isLE

theorem Hex.PermGroup.Generator.le_trans {n : Nat} {S : Array (Perm n)} (x y z : Generator S) (hxy : x.le y = true) (hyz : y.le z = true) : x.le z = true

theorem Hex.PermGroup.Generator.le_total {n : Nat} {S : Array (Perm n)} (x y : Generator S) : (x.le y || y.le x) = true

theorem Hex.PermGroup.Generator.before_of_le {n : Nat} {S : Array (Perm n)} {x y : Generator S} (hle : x.le y = true) (hne : x.value ≠ y.value) : Chain.before x.value y.value

def Hex.PermGroup.Generator.compact {n : Nat} {S : Array (Perm n)} : List (Generator S) → List (Generator S)

Remove adjacent equal values from a sorted list. Equal values keep the last input reference in their stable-sort block.

Equations

• Hex.PermGroup.Generator.compact [] = []
• Hex.PermGroup.Generator.compact (y :: ys) = match Hex.PermGroup.Generator.compact ys with | [] => [y] | y_1 :: ys => if y.value = y_1.value then y_1 :: ys else y :: y_1 :: ys

theorem Hex.PermGroup.Generator.compact_sublist {n : Nat} {S : Array (Perm n)} (xs : List (Generator S)) : (compact xs).Sublist xs

theorem Hex.PermGroup.Generator.mem_compact {n : Nat} {S : Array (Perm n)} (xs : List (Generator S)) (p : Perm n) : p ∈ List.map value (compact xs) ↔ p ∈ List.map value xs

theorem Hex.PermGroup.Generator.compact_sorted {n : Nat} {S : Array (Perm n)} (xs : List (Generator S)) (hs : List.Pairwise (fun (x y : Generator S) => x.le y = true) xs) : List.Pairwise (fun (x y : Generator S) => Chain.before x.value y.value) (compact xs)

def Hex.PermGroup.Generator.candidates {n : Nat} (S : Array (Perm n)) : List (Generator S)

Expand signed references in input-index order.

Equations

• Hex.PermGroup.Generator.candidates S = List.flatMap (fun (i : Fin S.size) => [Hex.PermGroup.Generator.ofIndex S i false, Hex.PermGroup.Generator.ofIndex S i true]) (List.finRange S.size)

theorem Hex.PermGroup.Generator.mem_candidates {n : Nat} (S : Array (Perm n)) (p : Perm n) : p ∈ List.map value (candidates S) ↔ ∃ (i : Fin S.size), p = S[↑i] ∨ p = S[↑i].inv

def Hex.PermGroup.Generator.ordered {n : Nat} (S : Array (Perm n)) : List (Generator S)

Sort the nonidentity signed inputs and keep one reference per permutation.

Equations

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

theorem Hex.PermGroup.Generator.mem_ordered {n : Nat} (S : Array (Perm n)) (p : Perm n) : p ∈ List.map value (ordered S) ↔ p ≠ Perm.id n ∧ ∃ (i : Fin S.size), p = S[↑i] ∨ p = S[↑i].inv

theorem Hex.PermGroup.Generator.ordered_pairwise {n : Nat} (S : Array (Perm n)) : List.Pairwise Chain.before (List.map value (ordered S))

theorem Hex.PermGroup.Generator.ordered_nodup {n : Nat} (S : Array (Perm n)) : (List.map value (ordered S)).Nodup

def Hex.PermGroup.Generator.program {n : Nat} {S : Array (Perm n)} (x : Generator S) : Program

A signed original-generator reference needs at most two program nodes.

Equations

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

theorem Hex.PermGroup.Generator.check_program {n : Nat} {S : Array (Perm n)} (x : Generator S) : checkWord S x.value x.program = true

structure Hex.PermGroup.Normalized {n : Nat} (S : Array (Perm n)) : Type

A normalized symmetric working array with checked provenance in the original input. Construction establishes both checker predicates unconditionally.

• generators : Array (Perm n)
• sources : Vector (Fin S.size × Bool) self.generators.size
• source_valid (j : Fin self.generators.size) : self.generators[↑j] = Word.letter S self.sources[↑j]
• words : Vector Program self.generators.size
• normalized : Chain.Normalized S self.generators
• valid : checkWords S self.generators self.words = true

def Hex.PermGroup.normalize {n : Nat} (S : Array (Perm n)) : Normalized S

Normalize without changing the original generator indexing used by programs.

Equations

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

theorem Hex.PermGroup.Normalized.symmetric {n : Nat} {S : Array (Perm n)} (c : Normalized S) (p : Perm n) (hp : p ∈ c.generators) : p.inv ∈ c.generators

theorem Hex.PermGroup.Normalized.generated_iff {n : Nat} {S : Array (Perm n)} (c : Normalized S) (p : Perm n) : Generated c.generators p ↔ Generated S p

theorem Hex.PermGroup.Normalized.fixed {n : Nat} {S : Array (Perm n)} (c : Normalized S) {base : Nat} (h : Chain.Fixed base S) : Chain.Fixed base c.generators

def Hex.PermGroup.Normalized.wordsFrom {n : Nat} {S : Array (Perm n)} (c : Normalized S) (words : Vector Program S.size) : Vector Program c.generators.size

Transfer provenance through the signed original references retained by normalization. Each output program uses one input program, optionally inverted.

Equations

• c.wordsFrom words = Hex.Vector.ofFn' fun (j : Fin c.generators.size) => let source := c.sources[↑j]; if source.snd = true then words[↑source.fst].inv else words[↑source.fst]

theorem Hex.PermGroup.Normalized.check_wordsFrom {n : Nat} {S : Array (Perm n)} (c : Normalized S) {T : Array (Perm n)} (words : Vector Program S.size) (h : checkWords T S words = true) : checkWords T c.generators (c.wordsFrom words) = true