theorem Hex.GraphIso.Nauty.childSt_count {n : Nat} {ctx : Ctx n} {st : RefineSt n} {level tc e o : Nat} (h : IterOk ctx level st) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (hacc : bcount st.ptn level n = st.numcells) : bcount (childSt ctx level st tc st.lab[tc + o]!).ptn (level + 1) n = (childSt ctx level st tc st.lab[tc + o]!).numcells

Individualization followed by refinement preserves an accurate cell count.

theorem Hex.GraphIso.Nauty.DescPath.equitable {n : Nat} {ctx : Ctx n} {base last : Nat} {root leaf : RefineSt n} {path : List (Nat × Nat)} (h : DescPath ctx base root path last leaf) (hok : IterOk ctx base root) (heq : Equitable ctx base root.lab root.ptn) (hacc : bcount root.ptn base n = root.numcells) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) : Equitable ctx last leaf.lab leaf.ptn ∧ bcount leaf.ptn last n = leaf.numcells

An equitable ancestor with an accurate cell count has equitable descendants with accurate counts, without any small-cell hypothesis.

theorem Hex.GraphIso.Nauty.GuidedPerm.equitable {n : Nat} {ctx : Ctx n} {store : Array Int} {tcLevel base level : Nat} {root current : RefineSt n} (h : GuidedPerm ctx tcLevel store base root level current) (hok : IterOk ctx base root) (heq : Equitable ctx base root.lab root.ptn) (hacc : bcount root.ptn base n = root.numcells) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) : Equitable ctx level current.lab current.ptn

Reordering within cells preserves the equitability of a guided endpoint.