theorem Hex.GraphIso.Nauty.SearchOut.ptn_eq {n k level numcells : Nat} {G : Colored n k} {st out : Search n} (h : SearchOut G level level st out) (hs : SearchOk G level numcells st) (ho : SearchOk G level numcells out) : out.ptn = st.ptn

Two valid states at the same sweep level agree on their whole partition when their search effect preserves every closed boundary.

theorem Hex.GraphIso.Nauty.Max.Loop.prepare_ok {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {l : Loop n} (h : Frame.Valid G l.node) : SearchOk G l.node.level (prepare ctx tcLevel l).fst (prepare ctx tcLevel l).snd.snd.snd.snd

A valid frozen node prepares a valid sweep partition.

theorem Hex.GraphIso.Nauty.Max.Loop.prepare_frame {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (l : Loop n) : have r := SearchState.refined ctx l.node.level l.node.numcells l.node.entry; have p := prepare ctx tcLevel l; p.fst = r.numcells ∧ p.snd.snd.snd.snd.lab = r.lab ∧ p.snd.snd.snd.snd.ptn = r.ptn

Preparing a sweep retains the refined partition and cell count.

theorem Hex.GraphIso.Nauty.Max.Parent.small {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {p : Parent n} (h : Valid G ctx tcLevel p) (hbase : SearchOk G p.loop.node.level (Loop.prepare ctx tcLevel p.loop).fst (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd) (hcheap : p.state.noncheaplevel ≤ p.loop.node.level) : SubtreeOk ctx p.loop.node.level (SearchState.refined ctx p.loop.node.level p.loop.node.numcells p.loop.node.entry)

A cheap suspended parent's current shape supplies the small-cell invariant at its frozen refined entry.

theorem Hex.GraphIso.Nauty.Max.Parent.cheap_key {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {p : Parent n} (h : Valid G ctx tcLevel p) (hbase : SearchOk G p.loop.node.level (Loop.prepare ctx tcLevel p.loop).fst (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd) (hsmall : SubtreeOk ctx p.loop.node.level (SearchState.refined ctx p.loop.node.level p.loop.node.numcells p.loop.node.entry)) (hselected : specTargetcell ctx (SearchState.refined ctx p.loop.node.level p.loop.node.numcells p.loop.node.entry).lab (SearchState.refined ctx p.loop.node.level p.loop.node.numcells p.loop.node.entry).ptn p.loop.node.level tcLevel = (Loop.prepare ctx tcLevel p.loop).snd.fst.toNat) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) : Frame.key ctx tcLevel p.loop.node = Frame.key ctx tcLevel (child ctx tcLevel p)

A small-cell parent with the specification target has exactly the key of its actual selected child, even after the parent was reordered.