def Hex.PermGroup.Chain.AllWorking {n : Nat} : Chain n → Prop

Every level of a chain, including the terminal one, has a symmetric working generator array.

Equations

• (Hex.PermGroup.Chain.leaf S words).AllWorking = Hex.PermGroup.Chain.Working S
• (Hex.PermGroup.Chain.cons level tail).AllWorking = (Hex.PermGroup.Chain.Working level.generators ∧ tail.AllWorking)

theorem Hex.PermGroup.Chain.AllWorking.working {n : Nat} {c : Chain n} (h : c.AllWorking) : Working c.generators

@[simp]

theorem Hex.PermGroup.Chain.allWorking_reword {n : Nat} (c : Chain n) (words : Vector Program c.generators.size) : (c.reword words).AllWorking ↔ c.AllWorking

def Hex.PermGroup.Chain.suffix {n : Nat} : Chain n → Chain n

The chain below the first level; a terminal chain is its own suffix.

Equations

• (Hex.PermGroup.Chain.leaf S words).suffix = Hex.PermGroup.Chain.leaf S words
• (Hex.PermGroup.Chain.cons level tail).suffix = tail

theorem Hex.PermGroup.Chain.AllWorking.suffix {n : Nat} {c : Chain n} (h : c.AllWorking) : c.suffix.AllWorking

theorem Hex.PermGroup.Chain.checkFrom_suffix {n : Nat} {c : Chain n} {base : Nat} (hb : base < n) (h : c.checkFrom base = true) : checkWords c.generators c.suffix.generators c.suffix.words = true ∧ c.suffix.checkFrom (base + 1) = true

def Hex.PermGroup.Normalized.ofWorking {n : Nat} (S : Array (Perm n)) (h : Chain.Working S) : Normalized S

A symmetric working array normalizes to itself, with one generator reference as the provenance of each element.

Equations

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

theorem Hex.PermGroup.Normalized.mem_push {n : Nat} {S : Array (Perm n)} (c : Normalized S) {p : Perm n} (d : Normalized (S.push p)) {x : Perm n} (hx : x ∈ c.generators) : x ∈ d.generators

Adding an input generator keeps every normalized generator.

def Hex.PermGroup.embedWord {n : Nat} (U : Array (Perm n)) (x : Perm n) : Program

A one-reference program for an element of U, or the identity if it is absent.

Equations

• Hex.PermGroup.embedWord U x = match U.finIdxOf? x with | some i => { nodes := #[Hex.PermGroup.Node.generator ↑i], root := 0 } | none => { nodes := #[Hex.PermGroup.Node.id], root := 0 }

theorem Hex.PermGroup.check_embedWord {n : Nat} (U : Array (Perm n)) {x : Perm n} (hx : x ∈ U) : checkWord U x (embedWord U x) = true

def Hex.PermGroup.embedWords {n : Nat} (U T : Array (Perm n)) : Vector Program T.size

Programs for the elements of T as references into an array U containing them.

Equations

• Hex.PermGroup.embedWords U T = Hex.Vector.ofFn' fun (j : Fin T.size) => Hex.PermGroup.embedWord U T[↑j]

theorem Hex.PermGroup.check_embedWords {n : Nat} (U T : Array (Perm n)) (h : ∀ (x : Perm n), x ∈ T → x ∈ U) : checkWords U T (embedWords U T) = true

def Hex.PermGroup.transferWords {n : Nat} (U : Array (Perm n)) {T R : Array (Perm n)} (h : ∀ (x : Perm n), x ∈ T → x ∈ U) (words : Vector Program R.size) (hw : checkWords T R words = true) : Vector Program R.size

Move programs over T to programs over a larger array U.

Equations

• Hex.PermGroup.transferWords U h words hw = Hex.Vector.ofFn' fun (j : Fin R.size) => Hex.PermGroup.Program.substitute U T (Hex.PermGroup.embedWords U T) ⋯ words[↑j] ⋯

theorem Hex.PermGroup.check_transferWords {n : Nat} (U : Array (Perm n)) {T R : Array (Perm n)} (h : ∀ (x : Perm n), x ∈ T → x ∈ U) (words : Vector Program R.size) (hw : checkWords T R words = true) : checkWords U R (transferWords U h words hw) = true

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

A complete suffix for a supplied input, retaining its normalization map for provenance transfer when used beneath another chain level.

• normal : Normalized S
• chain : Chain n
• generators : self.chain.generators = self.normal.generators
• checked : self.chain.checkFrom base = true
• words : checkWords S self.chain.generators self.chain.words = true
• working : self.chain.AllWorking
• extensions : Nat

  Strict subgroup insertions made while constructing this suffix, including those in its own suffixes.

theorem Hex.PermGroup.Construction.accepts_iff {n : Nat} {S : Array (Perm n)} {base : Nat} (c : Construction S base) (p : Perm n) : c.chain.accepts base p = true ↔ Generated S p

def Hex.PermGroup.Construction.reword {n : Nat} {S : Array (Perm n)} {base : Nat} (c : Construction S base) (words : Vector Program S.size) : Chain n

Give a complete suffix provenance in its preceding level.

Equations

• c.reword words = c.chain.reword (Vector.cast ⋯ (c.normal.wordsFrom words))

@[simp]

theorem Hex.PermGroup.Construction.reword_checked {n : Nat} {S : Array (Perm n)} {base : Nat} (c : Construction S base) (words : Vector Program S.size) : (c.reword words).checkFrom base = true

@[simp]

theorem Hex.PermGroup.Construction.reword_generators {n : Nat} {S : Array (Perm n)} {base : Nat} (c : Construction S base) (words : Vector Program S.size) : (c.reword words).generators = c.normal.generators

theorem Hex.PermGroup.Construction.reword_words {n : Nat} {S : Array (Perm n)} {base : Nat} (c : Construction S base) {T : Array (Perm n)} (words : Vector Program S.size) (hw : checkWords T S words = true) : checkWords T (c.reword words).generators (c.reword words).words = true

theorem Hex.PermGroup.Construction.reword_accepts {n : Nat} {S : Array (Perm n)} {base : Nat} (c : Construction S base) (words : Vector Program S.size) (p : Perm n) : (c.reword words).accepts base p = true ↔ Generated S p

theorem Hex.PermGroup.Construction.reword_working {n : Nat} {S : Array (Perm n)} {base : Nat} (c : Construction S base) (words : Vector Program S.size) : (c.reword words).AllWorking

def Hex.PermGroup.Construction.ofChain {n : Nat} (c : Chain n) (base : Nat) (hc : c.checkFrom base = true) (hw : c.AllWorking) : Construction c.generators base

Reuse a checked chain as a complete suffix for its own top-level generators.

Equations

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

structure Hex.PermGroup.Build.Seeds {n : Nat} (S : Array (Perm n)) (base : Nat) : Type

Retained generators, with provenance in the preceding level and fixed-point conditions for the complete suffix being rebuilt.

• generators : Array (Perm n)
• words : Vector Program self.generators.size
• valid : checkWords S self.generators self.words = true
• fixed : Chain.Fixed base self.generators

def Hex.PermGroup.Build.Seeds.empty {n : Nat} (S : Array (Perm n)) (base : Nat) : Seeds S base

Equations

• Hex.PermGroup.Build.Seeds.empty S base = { generators := #[], words := #v[], valid := ⋯, fixed := ⋯ }

def Hex.PermGroup.Build.Seeds.push {n : Nat} {S : Array (Perm n)} {base : Nat} (s : Seeds S base) (p : Perm n) (w : Program) (hw : checkWord S p w = true) (hf : ∀ (x : Fin n), ↑x < base → p.get x = x) : Seeds S base

Equations

• s.push p w hw hf = { generators := s.generators.push p, words := Vector.cast ⋯ (s.words.push w), valid := ⋯, fixed := ⋯ }

theorem Hex.PermGroup.Build.Seeds.push_mono {n : Nat} {S : Array (Perm n)} {base : Nat} (s : Seeds S base) (p : Perm n) (w : Program) (hw : checkWord S p w = true) (hf : ∀ (x : Fin n), ↑x < base → p.get x = x) {q : Perm n} (hq : Generated s.generators q) : Generated (s.push p w hw hf).generators q

theorem Hex.PermGroup.Build.Seeds.push_mem {n : Nat} {S : Array (Perm n)} {base : Nat} (s : Seeds S base) (p : Perm n) (w : Program) (hw : checkWord S p w = true) (hf : ∀ (x : Fin n), ↑x < base → p.get x = x) : Generated (s.push p w hw hf).generators p

structure Hex.PermGroup.Build.State {n : Nat} (S : Array (Perm n)) (base : Nat) : Type

Filtering always keeps a complete chain for exactly the retained generators.

• seeds : Seeds S base
• result : Construction self.seeds.generators base
• extensions : Nat

  Extensions made so far, including those inside suffix extensions.

structure Hex.PermGroup.Build.Candidate {n : Nat} (S : Array (Perm n)) (base : Nat) : Type

A candidate's program is delayed until insertion, so discarded Schreier elements allocate neither copied transporter programs nor provenance arrays.

• value : Perm n
• word : Unit → Program
• valid : checkWord S self.value (self.word ()) = true
• fixed (x : Fin n) : ↑x < base → self.value.get x = x

@[reducible, inline]

abbrev Hex.PermGroup.Build.Extender (n base : Nat) : Type

Extend a complete suffix by one input generator.

Equations

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

def Hex.PermGroup.Build.State.insert {n : Nat} {S : Array (Perm n)} {base : Nat} (extend : Extender n base) (s : State S base) (p : Perm n) (w : Unit → Program) (hw : checkWord S p (w ()) = true) (hf : ∀ (x : Fin n), ↑x < base → p.get x = x) : State S base

Inspect one candidate using a complete sift. A successful sift leaves the state alone; a failure inserts the generator and extends the current suffix.

Equations

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

theorem Hex.PermGroup.Build.State.insert_mono {n : Nat} {S : Array (Perm n)} {base : Nat} (build : Extender n base) (s : State S base) (p : Perm n) (w : Unit → Program) (hw : checkWord S p (w ()) = true) (hf : ∀ (x : Fin n), ↑x < base → p.get x = x) {q : Perm n} (hq : Generated s.seeds.generators q) : Generated (insert build s p w hw hf).seeds.generators q

theorem Hex.PermGroup.Build.State.insert_mem {n : Nat} {S : Array (Perm n)} {base : Nat} (build : Extender n base) (s : State S base) (p : Perm n) (w : Unit → Program) (hw : checkWord S p (w ()) = true) (hf : ∀ (x : Fin n), ↑x < base → p.get x = x) : Generated (insert build s p w hw hf).seeds.generators p

theorem Hex.PermGroup.Build.State.insert_strict {n : Nat} {S : Array (Perm n)} {base : Nat} (build : Extender n base) (s : State S base) (p : Perm n) (w : Unit → Program) (hw : checkWord S p (w ()) = true) (hf : ∀ (x : Fin n), ↑x < base → p.get x = x) (h : s.result.chain.accepts base p = false) : ¬Generated s.seeds.generators p ∧ Generated (insert build s p w hw hf).seeds.generators p

A failed complete sift supplies a witness that insertion strictly enlarges the retained subgroup. The same claim is not made for an unfinished chain.

def Hex.PermGroup.Build.State.scan {n : Nat} {S : Array (Perm n)} {base : Nat} {ι : Type} (build : Extender n base) (family : ι → Candidate S base) (s : State S base) : List ι → State S base

Stream candidates in their supplied order, extending the suffix only after an exact nonmembership verdict from the current complete suffix.

Equations

• Hex.PermGroup.Build.State.scan build family s [] = s
• Hex.PermGroup.Build.State.scan build family s (i :: is) = Hex.PermGroup.Build.State.scan build family (Hex.PermGroup.Build.State.insert build s (family i).value (family i).word ⋯ ⋯) is

theorem Hex.PermGroup.Build.State.scan_mono {n : Nat} {S : Array (Perm n)} {base : Nat} {ι : Type} (build : Extender n base) (family : ι → Candidate S base) (s : State S base) (is : List ι) {p : Perm n} (hp : Generated s.seeds.generators p) : Generated (scan build family s is).seeds.generators p

theorem Hex.PermGroup.Build.State.scan_mem {n : Nat} {S : Array (Perm n)} {base : Nat} {ι : Type} (build : Extender n base) (family : ι → Candidate S base) (s : State S base) (is : List ι) (i : ι) (hi : i ∈ is) : Generated (scan build family s is).seeds.generators (family i).value

def Hex.PermGroup.Build.family {n : Nat} {S : Array (Perm n)} {base : Nat} (hbase : base < n) (normal : Normalized S) (hf : Chain.Fixed base S) (orbit : { c : Orbit n // Orbit.Valid normal.generators ⟨base, hbase⟩ c }) (pair : Fin normal.generators.size × Fin orbit.val.points.size) : Candidate normal.generators (base + 1)

The Schreier candidates of one level: h(s, x) for each symmetric generator s and orbit point x, with delayed words in the level generators.

Equations

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

def Hex.PermGroup.Build.pairs (r q : Nat) : List (Fin r × Fin q)

All Schreier pairs of a level, generator-major.

Equations

• Hex.PermGroup.Build.pairs r q = List.flatMap (fun (i : Fin r) => List.map (fun (x : Fin q) => (i, x)) (List.finRange q)) (List.finRange r)

theorem Hex.PermGroup.Build.mem_pairs {r q : Nat} (i : Fin r) (x : Fin q) : (i, x) ∈ pairs r q

def Hex.PermGroup.Build.assemble {n : Nat} {S : Array (Perm n)} {base : Nat} (hbase : base < n) (normal : Normalized S) (hf : Chain.Fixed base S) (orbit : { c : Orbit n // Orbit.Valid normal.generators ⟨base, hbase⟩ c }) (result : State normal.generators (base + 1)) (hall : ∀ (pair : Fin normal.generators.size × Fin orbit.val.points.size), Generated result.seeds.generators (family hbase normal hf orbit pair).value) : Construction S base

Assemble a level from a final scan state whose retained generators generate every Schreier candidate of the level.

Equations

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

def Hex.PermGroup.Build.complete {n : Nat} {S : Array (Perm n)} {base : Nat} (hbase : base < n) (normal : Normalized S) (hf : Chain.Fixed base S) (orbit : { c : Orbit n // Orbit.Valid normal.generators ⟨base, hbase⟩ c }) (extend : Extender n (base + 1)) (initial : State normal.generators (base + 1)) : Construction S base

Complete one level from a starting state for its suffix: stream every Schreier pair against the current complete suffix, extending it at each rejection. The starting state may already contain retained generators.

Equations

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

def Hex.PermGroup.Build.terminal {n : Nat} {S : Array (Perm n)} {base : Nat} (hbase : ¬base < n) (hb : base ≤ n) (normal : Normalized S) (hf : Chain.Fixed base S) : Construction S base

The terminal level: every generator fixes every point.

Equations

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

def Hex.PermGroup.Build.resume {n : Nat} {S : Array (Perm n)} {base : Nat} (hbase : base < n) (c : Construction S base) {p : Perm n} (normal : Normalized (S.push p)) : State normal.generators (base + 1)

The starting state for extending a complete suffix by one generator: the suffix below its first level, with provenance moved to the new level's generators, which contain the old ones.

Equations

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

@[irreducible]

def Hex.PermGroup.Build.extend {n : Nat} (base : Nat) (hb : base ≤ n) (S : Array (Perm n)) (c : Construction S base) (p : Perm n) (hf : Chain.Fixed base (S.push p)) : Construction (S.push p) base

Add one generator to a complete suffix. The previous suffix below this level becomes the starting state of the new level's scan, so only Schreier generators that it rejects cause recursive extensions; nothing is rebuilt from scratch.

Equations

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

@[irreducible]

def Hex.PermGroup.Build.empty {n : Nat} (base : Nat) (hb : base ≤ n) : Construction #[] base

A complete chain for the trivial subgroup.

Equations

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

def Hex.PermGroup.Build.build {n : Nat} (base : Nat) (hb : base ≤ n) (S : Array (Perm n)) (hf : Chain.Fixed base S) : Construction S base

Deterministic Schreier-Sims construction. The first level streams its Schreier generators against a complete chain for those retained so far, starting from the trivial chain and extended at each rejection; that chain is the suffix.

Equations

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

def Hex.PermGroup.Group.ofGenerators {n : Nat} (S : Array (Perm n)) : Group n

Construct a complete checked group for every input generator array. Original indices are retained even when normalization removes identities or duplicates.

Equations

• Hex.PermGroup.Group.ofGenerators S = { generators := S, chain := (Hex.PermGroup.Build.build 0 ⋯ S ⋯).chain, valid := ⋯ }

theorem Hex.PermGroup.Group.ofGenerators_checks {n : Nat} (S : Array (Perm n)) : checkChain S (ofGenerators S).chain = true

@[simp]

theorem Hex.PermGroup.Group.generators_ofGenerators {n : Nat} (S : Array (Perm n)) : (ofGenerators S).generators = S

theorem Hex.PermGroup.Group.contains_ofGenerators {n : Nat} (S : Array (Perm n)) (p : Perm n) : (ofGenerators S).contains p = true ↔ Generated S p