def Hex.PermGroup.Blocks.images {n : Nat} (S : Array (Perm n)) (x y : Fin n) : List (Fin n × Fin n)

Pending generator images in the supplied generator order.

Equations

• Hex.PermGroup.Blocks.images S x y = List.map (fun (s : Hex.Perm n) => (s.get x, s.get y)) S.toList

def Hex.PermGroup.Blocks.Closed {n : Nat} (S : Array (Perm n)) (p : Partition n) (todo : List (Fin n × Fin n)) : Prop

Closure obligations are retained in the pending queue. Any equivalence relation containing both the current blocks and the queue must contain the generator images of the current blocks.

Equations

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

def Hex.PermGroup.Blocks.Covers {n : Nat} (seeds : List (Fin n × Fin n)) (p : Partition n) (todo : List (Fin n × Fin n)) : Prop

The processed blocks together with the queue still imply every input seed.

Equations

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

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

An effective-union trace and the proof invariants of its FIFO queue. Only the trace survives proof erasure.

• trace : List (Fin n × Fin n)
• replayed : replay S seeds (Partition.discrete n) self.trace = some p
• pending (q : Fin n × Fin n) : q ∈ todo → Forced S seeds p q.fst q.snd
• closed : Closed S p todo
• covers : Covers seeds p todo

def Hex.PermGroup.Blocks.State.initial {n : Nat} (S : Array (Perm n)) (seeds : List (Fin n × Fin n)) : State S seeds (Partition.discrete n) seeds

Start with singleton blocks and the supplied seed queue.

Equations

• Hex.PermGroup.Blocks.State.initial S seeds = { trace := [], replayed := ⋯, pending := ⋯, closed := ⋯, covers := ⋯ }

def Hex.PermGroup.Blocks.State.skip {n : Nat} {S : Array (Perm n)} {seeds : List (Fin n × Fin n)} {p : Partition n} {x y : Fin n} {todo : List (Fin n × Fin n)} (st : State S seeds p ((x, y) :: todo)) (h : p.Same x y) : State S seeds p todo

Drop a request whose two points are already joined.

Equations

• st.skip h = { trace := st.trace, replayed := ⋯, pending := ⋯, closed := ⋯, covers := ⋯ }

def Hex.PermGroup.Blocks.State.merge {n : Nat} {S : Array (Perm n)} {seeds : List (Fin n × Fin n)} {p : Partition n} {x y : Fin n} {todo : List (Fin n × Fin n)} (st : State S seeds p ((x, y) :: todo)) (h : ¬p.Same x y) : State S seeds (p.merge x y) (todo ++ images S x y)

Join the requested blocks and enqueue one image pair per generator. Previously queued requests remain justified after this coarsening.

Equations

• st.merge h = { trace := st.trace ++ [(x, y)], replayed := ⋯, pending := ⋯, closed := ⋯, covers := ⋯ }

theorem Hex.PermGroup.Blocks.State.check {n : Nat} {S : Array (Perm n)} {seeds : List (Fin n × Fin n)} {p : Partition n} (st : State S seeds p []) : Blocks.check S seeds p st.trace = true

Empty pending queues give complete checked block systems.