theorem Hex.GraphIso.Nauty.Generation.cellStab_fixes {ptn lab γ : Array Nat} {level pos : Nat} (hpos : pos < lab.size) (hcell : IsCell ptn level pos 1) (h : CellStab ptn level lab γ) : γ[lab[pos]!]! = lab[pos]!

A cell-stabilizing array fixes every vertex in a singleton cell.

theorem Hex.GraphIso.Nauty.Generation.frame_fixes {n : Nat} {base : List (Fin n)} {level : Nat} {st : Search n} {γ : Array Nat} (hfixed : FixedCells level st) (hsize : st.lab.size = n) (hbase : ∀ (b : Fin n), b ∈ base → st.fixedpts.mem ↑b = true) (hstab : CellStab st.ptn level st.lab γ) (b : Fin n) : b ∈ base → γ[↑b]! = ↑b

Stabilizing a reached frame fixes the individualized base because those vertices are singleton cells in that frame.