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

A full discovery queue and proof that another reachable object exists. Exhaustion supplies positive information only, with no coverage claim.

• queue : a.Queue x
• full : self.queue.objects.size = cap
• more : ∃ (y : α), (∃ (p : Element G), a.act p x = y) ∧ ¬y ∈ self.queue.objects

def Hex.PermGroup.Action.Queue.visit {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} (cap : Nat) (t : a.Queue x) (ht : t.objects.size ≤ cap) (i : Fin t.objects.size) (s : Step G) : Except (a.Exhausted x cap) { u : a.Queue x // t.Extends u ∧ a.act s.element t.objects[↑i] ∈ u.objects ∧ u.objects.size ≤ cap }

Equations

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

def Hex.PermGroup.Action.Queue.scan {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} (cap : Nat) (t : a.Queue x) (ht : t.objects.size ≤ cap) (i : Fin t.objects.size) (steps : List (Step G)) : Except (a.Exhausted x cap) { u : a.Queue x // t.Extends u ∧ (∀ (s : Step G), s ∈ steps → a.act s.element t.objects[↑i] ∈ u.objects) ∧ u.objects.size ≤ cap }

Visit signed generators in their fixed input order. An exhausted traversal retains the last full queue, including discoveries made earlier in this scan.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Action.Queue.scan cap t ht i [] = Except.ok ⟨t, ⋯⟩

theorem Hex.PermGroup.Action.Queue.scan_processed {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} {t u : a.Queue x} (cursor : Nat) (hc : cursor < t.objects.size) (hp : t.Processed cursor) (he : t.Extends u) (hs : ∀ (s : Step G), s ∈ Step.all G → a.act s.element t.objects[cursor] ∈ u.objects) : u.Processed (cursor + 1)

@[irreducible]

def Hex.PermGroup.Action.Queue.finish {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} (cap : Nat) (t : a.Queue x) (ht : t.objects.size ≤ cap) (cursor : Nat) (hp : t.Processed cursor) : Except (a.Exhausted x cap) { c : Orbit G α // Orbit.Valid a x c ∧ c.objects.size ≤ cap ∧ ∀ (i : Fin c.objects.size), c.words[↑i].nodes.size ≤ 3 * cap }

The cursor advances once for each discovered object. The checked object cap is the termination bound; it does not require allocating an ambient domain.

Equations

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

inductive Hex.PermGroup.Action.OrbitLimit {x✝ : Nat} {G : Group x✝} {α : Type u_1} (a : Action G α) (x : α) (cap : Nat) : Type u_1

Insufficient object capacity, including the inability to store the base.

• zero {x✝ : Nat} {G : Group x✝} {α : Type u_1} {a : Action G α} {x : α} {cap : Nat} (empty : cap = 0) : a.OrbitLimit x cap
• full {x✝ : Nat} {G : Group x✝} {α : Type u_1} {a : Action G α} {x : α} {cap : Nat} (exhausted : a.Exhausted x cap) : a.OrbitLimit x cap

def Hex.PermGroup.Action.breadthFirst {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] (a : Action G α) (x : α) (cap : Nat) : Except (a.OrbitLimit x cap) { c : Orbit G α // Orbit.Valid a x c ∧ c.objects.size ≤ cap ∧ ∀ (i : Fin c.objects.size), c.words[↑i].nodes.size ≤ 3 * cap }

Deterministic BFS on just the requested orbit, retaining checked words in the original generators. It never enumerates all tuples, subsets or partitions.

Equations

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

theorem Hex.PermGroup.Action.Exhausted.tooSmall_domain {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {cap : Nat} (e : a.Exhausted x cap) (objects : Array α) (hd : a.Domain objects) (hx : x ∈ objects) : cap < objects.size

Every invariant domain containing the base needs room for the full queue and the additional reachable object witnessed by exhaustion.

theorem Hex.PermGroup.Action.Exhausted.tooSmall {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {cap : Nat} (e : a.Exhausted x cap) (c : Orbit G α) (hc : Orbit.Valid a x c) : cap < c.objects.size

theorem Hex.PermGroup.Action.OrbitLimit.tooSmall_domain {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {cap : Nat} (e : a.OrbitLimit x cap) (objects : Array α) (hd : a.Domain objects) (hx : x ∈ objects) : cap < objects.size

theorem Hex.PermGroup.Action.OrbitLimit.tooSmall {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {cap : Nat} (e : a.OrbitLimit x cap) (c : Orbit G α) (hc : Orbit.Valid a x c) : cap < c.objects.size

theorem Hex.PermGroup.Action.breadthFirst_complete {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] (a : Action G α) (x : α) (cap : Nat) (c : Orbit G α) (hc : Orbit.Valid a x c) (hs : c.objects.size ≤ cap) : ∃ (result : { c : Orbit G α // Orbit.Valid a x c ∧ c.objects.size ≤ cap ∧ ∀ (i : Fin c.objects.size), c.words[↑i].nodes.size ≤ 3 * cap }), a.breadthFirst x cap = Except.ok result

A sufficient object budget guarantees completion, without assuming that the action is faithful or enumerating the ambient type.

def Hex.PermGroup.Action.orbitOfDomain {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] (a : Action G α) (objects : Array α) (hd : a.Domain objects) (x : α) (hx : x ∈ objects) : { c : Orbit G α // Orbit.Valid a x c ∧ c.objects.size ≤ objects.size ∧ ∀ (i : Fin c.objects.size), c.words[↑i].nodes.size ≤ 3 * objects.size }

An invariant finite domain bounds every orbit it contains. The traversal still discovers only this orbit, without copying the rest of the domain.

Equations

• a.orbitOfDomain objects hd x hx = match a.breadthFirst x objects.size with | Except.ok result => result | Except.error e => ⋯.elim