theorem Hex.PermGroup.checkOrbit_spec {n : ℕ} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : checkOrbit S a c = true) (x : Fin n) : x ∈ c.points ↔ ∃ e ∈ closure S, e a = x

A checked orbit is the full orbit of Mathlib's generated subgroup.

theorem Hex.PermGroup.closure_stabilizerGens {n : ℕ} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Orbit.Valid S a c) : closure (Orbit.stabilizerGens h) = closure S ⊓ MulAction.stabilizer (Equiv.Perm (Fin n)) a

The Schreier generators describe the subgroup intersection with the ambient point stabilizer, retaining the declared permutation degree.