structure Hex.PermGroup.Blocks.Solution {n : Nat} (S : Array (Perm n)) (seeds : List (Fin n × Fin n)) : Type

A canonical minimal invariant partition with its independently replayable sequence of forced unions.

• partition : Partition n
• trace : List (Fin n × Fin n)
• checked : check S seeds self.partition self.trace = true

@[irreducible]

def Hex.PermGroup.Blocks.run {n : Nat} (S : Array (Perm n)) (seeds : List (Fin n × Fin n)) (p : Partition n) (todo : List (Fin n × Fin n)) (st : State S seeds p todo) : Solution S seeds

Process the FIFO queue until no closure obligations remain. Effective merges decrease the block count; redundant requests decrease the queue length.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Blocks.run S seeds p [] st_2 = { partition := p, trace := st_2.trace, checked := ⋯ }

def Hex.PermGroup.Blocks.solve {n : Nat} (S : Array (Perm n)) (seeds : List (Fin n × Fin n)) : Solution S seeds

Least invariant equivalence relation containing arbitrary independent seed pairs. Only effective unions enqueue generator images.

Equations

• Hex.PermGroup.Blocks.solve S seeds = Hex.PermGroup.Blocks.run S seeds (Hex.PermGroup.Partition.discrete n) seeds (Hex.PermGroup.Blocks.State.initial S seeds)

theorem Hex.PermGroup.Blocks.Solution.admissible {n : Nat} {S : Array (Perm n)} {seeds : List (Fin n × Fin n)} (s : Solution S seeds) : Admissible S seeds s.partition.Same

theorem Hex.PermGroup.Blocks.Solution.least {n : Nat} {S : Array (Perm n)} {seeds : List (Fin n × Fin n)} (s : Solution S seeds) (R : Fin n → Fin n → Prop) (hR : Admissible S seeds R) : s.partition.Refines R

theorem Hex.PermGroup.Blocks.Solution.unique {n : Nat} {S : Array (Perm n)} {seeds : List (Fin n × Fin n)} (s t : Solution S seeds) : s.partition = t.partition

Any two accepted solutions have the same canonical partition.

theorem Hex.PermGroup.Blocks.Solution.trace_bound {n : Nat} {S : Array (Perm n)} {seeds : List (Fin n × Fin n)} (s : Solution S seeds) : s.trace.length ≤ n - 1

At most n-1 unions are needed; degree zero has an empty trace.