theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.singleton_const {n level : Nat} {s : RefineSt n} (h : Valid level s) (G : SparseGraph n) (split : Nat) (hb : split < n) : have t := splitSingleton (Graph.ofGraph G) level split s; ∀ (a len : Nat), IsCell t.ptn level a len → a + len ≤ n → ConstOn (Graph.context G) (worksetOf n s.lab split split) (segN t.lab a len)

The complete singleton pass stabilizes its captured splitter in the shared equitability predicate, using native row counts.

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.nontrivial_const {n level : Nat} {s : RefineSt n} (h : Valid level s) (G : SparseGraph n) (split len : Nat) (hc : IsCell s.ptn level split len) (hb : split + len ≤ n) : have t := splitNontrivial (Graph.ofGraph G) level split s; ∀ (a size : Nat), IsCell t.ptn level a size → a + size ≤ n → ConstOn (Graph.context G) (worksetOf n s.lab split s.cellend[split]!) (segN t.lab a size)

The complete nontrivial pass stabilizes its captured splitter in the shared equitability predicate, including untouched zero-count cells.