structure Hex.PermGroup.Action.Queue {x✝ : Nat} {G : Group x✝} {α : Type u_1} (a : Action G α) (x : α) : Type u_1

A breadth-first queue with shared transporter programs. Each object is reachable, but closure is deliberately absent until traversal completes.

• objects : Array α
• arena : Program.Builder G.generators
• roots : Vector Nat self.objects.size
• bound (i : Fin self.objects.size) : self.roots[↑i] < self.arena.values.size
• nodup : self.objects.toList.Nodup
• base : x ∈ self.objects
• image (i : Fin self.objects.size) : a.act self.arena.values[self.roots[↑i]] x = self.objects[↑i]
• identity (i : Fin self.objects.size) : self.objects[↑i] = x → self.arena.values[self.roots[↑i]] = Element.id G
• nodes_le : self.arena.nodes.size ≤ 3 * self.objects.size

def Hex.PermGroup.Action.Queue.root {n : Nat} {G : Group n} {α : Type u} (a : Action G α) (x : α) : a.Queue x

Equations

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

def Hex.PermGroup.Action.Queue.push {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} (t : a.Queue x) (i : Fin t.objects.size) (s : Step G) (hnew : ¬a.act s.element t.objects[↑i] ∈ t.objects) : a.Queue x

Extend only after checking that this neighbor has not been discovered.

Equations

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

structure Hex.PermGroup.Action.Queue.Extends {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} (t u : a.Queue x) : Prop

Extension preserves discovery indices.

• size : t.objects.size ≤ u.objects.size
• get (i : Fin t.objects.size) : u.objects[↑i] = t.objects[↑i]

theorem Hex.PermGroup.Action.Queue.Extends.refl {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} (t : a.Queue x) : t.Extends t

theorem Hex.PermGroup.Action.Queue.Extends.trans {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} {t u v : a.Queue x} (htu : t.Extends u) (huv : u.Extends v) : t.Extends v

theorem Hex.PermGroup.Action.Queue.Extends.mem {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} {t u : a.Queue x} (h : t.Extends u) {y : α} (hy : y ∈ t.objects) : y ∈ u.objects

theorem Hex.PermGroup.Action.Queue.push_extends {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} (t : a.Queue x) (i : Fin t.objects.size) (s : Step G) (hnew : ¬a.act s.element t.objects[↑i] ∈ t.objects) : t.Extends (t.push i s hnew)

def Hex.PermGroup.Action.Queue.orbit {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} (t : a.Queue x) : Orbit G α

Export all transporter roots against their one shared node array.

Equations

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

theorem Hex.PermGroup.Action.Queue.orbit_nodes {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} (t : a.Queue x) (i : Fin t.objects.size) : t.orbit.words[↑i].nodes.size ≤ 3 * t.objects.size

theorem Hex.PermGroup.Action.Queue.reachable {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} (t : a.Queue x) (y : α) (hy : y ∈ t.objects) : ∃ (p : Element G), a.act p x = y

def Hex.PermGroup.Action.Queue.Processed {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} (t : a.Queue x) (cursor : Nat) : Prop

All signed edges from the first cursor entries have been inspected.

Equations

• t.Processed cursor = ∀ (i : Fin t.objects.size), ↑i < cursor → ∀ (s : Hex.PermGroup.Action.Step G), a.act s.element t.objects[↑i] ∈ t.objects

theorem Hex.PermGroup.Action.Queue.orbit_valid {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} (t : a.Queue x) (hc : t.Processed t.objects.size) : Orbit.Valid a x t.orbit