theorem Hex.PermGroup.Action.Queue.reps_nodup {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} (t : a.Queue x) : t.orbit.reps.toList.Nodup

theorem Hex.PermGroup.Action.Exhausted.tooSmall_order {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} {cap : Nat} (e : a.Exhausted x cap) : cap < G.order

Distinct discovered objects require distinct group elements. This counting argument is erased; traversal never enumerates the group.

theorem Hex.PermGroup.Action.OrbitLimit.tooSmall_order {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} {cap : Nat} (e : a.OrbitLimit x cap) : cap < G.order

theorem Hex.PermGroup.Action.exists_orbit {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] (a : Action G α) (x : α) : ∃ (c : Orbit G α), Orbit.Valid a x c

Every action orbit is finite. Existence is proved using the group-order bound; clients retain their own explicit, usually much smaller object budgets.