structure Hex.GraphIso.Nauty.NodePre {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel level numcells : Nat) (st : Search n) : Prop

An off-path node carries the pending history of its actual refinement.

• positive : 1 ≤ level
• partition : SearchOk G level numcells st
• stored : RunInv G ctx st
• ancestor : st.gcaFirst < level
• canonAncestor : st.gcaCanon < level
• history : let r := visit ctx level numcells st; History ctx tcLevel level (level - 1) r.fst r.snd.snd
• equitable : Equitable ctx level (SearchState.refined ctx level numcells st).lab (SearchState.refined ctx level numcells st).ptn
• boundary : Boundary G ctx level st
• cheapBound : st.noncheaplevel ≤ level
• path : PathInv G ctx level st
• starts (v : Nat) : st.active.mem v = true → v = 0 ∨ st.ptn[v - 1]! ≤ level
• small : st.noncheaplevel < level → NodeShape n level (SearchState.refined ctx level numcells st).ptn

structure Hex.GraphIso.Nauty.SweepPre {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel : Nat) (first : Bool) (level numcells tc tv1 : Nat) (cursor : Option Nat) (cell : VSet n) (st : Search n) : Prop

A later-sibling sweep retains the parent history and its recorded target.

• past : Generic.Past first tv1 cursor
• positive : 1 ≤ level
• partition : SearchOk G level numcells st
• target : Generic.Target (fun (st : Search n) => st) level tc cell st
• cursor_mem (v : Nat) : cursor = some v → cell.mem v = true
• stored : RunInv G ctx st
• ancestor : st.gcaFirst ≤ level
• canonAncestor : st.gcaCanon ≤ level
• history : History ctx tcLevel level level numcells st
• recorded : Recorded ctx tcLevel level tc st
• equitable : Equitable ctx level st.lab st.ptn
• boundary : Boundary G ctx (level + 1) st
• cheapBound : st.noncheaplevel ≤ level + 1
• path : PathInv G ctx level st
• small : st.noncheaplevel ≤ level → NodeShape n level st.ptn

theorem Hex.GraphIso.Nauty.NodePre.subtree {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (h : NodePre G ctx tcLevel level numcells st) (hn0 : 0 < n) (hc : st.noncheaplevel < level) : SubtreeOk ctx level (SearchState.refined ctx level numcells st)

Below a saved cheap boundary, the actual refined node satisfies the small-cell theorem's complete geometric and equitable invariant.

theorem Hex.GraphIso.Nauty.SweepPre.subtree {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells tc tv1 : Nat} {first : Bool} {cursor : Option Nat} {cell : VSet n} {st : Search n} (h : SweepPre G ctx tcLevel first level numcells tc tv1 cursor cell st) (hn0 : 0 < n) (hc : st.noncheaplevel ≤ level) : SubtreeOk ctx level { lab := st.lab, ptn := st.ptn, active := st.active, numcells := numcells, hint := 0, maxpos := 0, longcode := 0 }

A cheap sweep supplies the small-cell invariant for its current parent partition, including after a descendant has returned and recovery ran.

theorem Hex.GraphIso.Nauty.SweepPre.local_pairs {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells tc tv1 : Nat} {first : Bool} {cursor : Option Nat} {cell : VSet n} {st : Search n} (h : SweepPre G ctx tcLevel first level numcells tc tv1 cursor cell st) : LocalAutos ctx level st

At a resumed sweep, every pair passing its fix test has realizers stabilizing the partition where the filter is applied.