theorem Hex.GraphIso.Nauty.Max.extend_refinement {n k : Nat} {G : Colored n k} {t level nc mc : Nat} {base st out : Search n} (ht : 1 ≤ t) (htl : t < level) (hb : SearchOk G t nc base) (hs : SearchOk G level mc st) (he : SearchOut G t t base st) (ho : SearchOut G (level - 1) level st out) : SearchOut G t t base out

A node refinement preserves every strictly older ancestor frame.

theorem Hex.GraphIso.Nauty.Max.NodeInput.singletons {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel : Nat} {first : Bool} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : NodeInput G ctx tcLevel fuel first f bs fs parents) {t : Nat} {p : Parent n} (hp : parents t = some p) : IsCell f.entry.ptn f.level (Loop.prepare ctx tcLevel p.loop).snd.fst.toNat 1

Ancestor chosen vertices are singletons at the actual node entry.

theorem Hex.GraphIso.Nauty.Max.NodeInput.prepare_scope {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel : Nat} {first : Bool} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : NodeInput G ctx tcLevel fuel first f bs fs parents) : have l := { node := f, first := first }; have out := (Loop.prepare ctx tcLevel l).snd.snd.snd.snd; Scope G ctx tcLevel f.level (Loop.codes ctx l) bs out parents

Preparing a node preserves every saved ancestor and extends the actual code prefix consumed by its child sweep.

theorem Hex.GraphIso.Nauty.Max.NodeInput.prepare_counters {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel : Nat} {first : Bool} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : NodeInput G ctx tcLevel fuel first f bs fs parents) : have l := { node := f, first := first }; have st := (Loop.prepare ctx tcLevel l).snd.snd.snd.snd; 0 < st.canonlevel → 0 < st.gcaFirst ∧ st.gcaFirst ≤ st.gcaCanon

The initialized sweep inherits the node's installed-reference counters.

theorem Hex.GraphIso.Nauty.Max.Loop.first_shape {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {l : Loop n} (h : Frame.Valid G l.node) (hf : l.first = true) (hnc : (prepare ctx tcLevel l).fst < n) : have p := prepare ctx tcLevel l; IsCell p.snd.snd.snd.snd.ptn l.node.level p.snd.fst.toNat p.snd.snd.snd.fst ∧ 2 ≤ p.snd.snd.snd.fst ∧ p.snd.fst.toNat + p.snd.snd.snd.fst ≤ n ∧ p.snd.snd.fst = windowSet n p.snd.snd.snd.snd.lab p.snd.fst.toNat p.snd.snd.snd.fst

The first internal node selects the whole actual nontrivial cell.

theorem Hex.GraphIso.Nauty.Max.NodeInput.first_input {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : NodeInput G ctx tcLevel (fuel + 1) true f bs fs parents) (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) (hnc : (Generic.prepareFirst ctx tcLevel f.level f.numcells f.entry).fst ≠ n) : have l := { node := f, first := true }; have p := Loop.prepare ctx tcLevel l; SweepInput G ctx tcLevel fuel (n + 1) true f.level p.fst p.snd.fst.toNat ((p.snd.snd.fst.nextElem none).getD 0) (p.snd.snd.fst.nextElem none) p.snd.snd.fst 0 p.snd.snd.snd.snd l bs fs parents

The first internal node initializes the complete sweep contract at its actual prepared state, before any child has been covered.

theorem Hex.GraphIso.Nauty.Max.target_active {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (hnc : numcells < n) (hi : (classify ctx level numcells (chooseTarget false ctx tcLevel level numcells st).snd.snd.snd).fst = Generic.Leaf.internal) : st.eqlevFirst = level ∨ 0 ≤ st.compCanon

An off-path internal classification requires an active target.

theorem Hex.GraphIso.Nauty.Max.Loop.other_shape {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {l : Loop n} (h : Frame.Valid G l.node) (hf : l.first = false) (hnc : (prepare ctx tcLevel l).fst < n) (hi : have p := prepareOther ctx tcLevel l.node.level l.node.numcells l.node.entry; (classify ctx l.node.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.internal) : have p := prepare ctx tcLevel l; IsCell p.snd.snd.snd.snd.ptn l.node.level p.snd.fst.toNat p.snd.snd.snd.fst ∧ 2 ≤ p.snd.snd.snd.fst ∧ p.snd.fst.toNat + p.snd.snd.snd.fst ≤ n ∧ p.snd.snd.fst = windowSet n p.snd.snd.snd.snd.lab p.snd.fst.toNat p.snd.snd.snd.fst

The off-path internal node selects a complete target window, including the hinted target used while harvesting generators in a dominated tree.

theorem Hex.GraphIso.Nauty.Max.NodeInput.other_input {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : NodeInput G ctx tcLevel (fuel + 1) false f bs fs parents) (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) (hinternal : have p := prepareOther ctx tcLevel f.level f.numcells f.entry; (classify ctx f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.internal) : have l := { node := f, first := false }; have p := Loop.prepare ctx tcLevel l; SweepInput G ctx tcLevel fuel (n + 1) false f.level p.fst p.snd.fst.toNat ((p.snd.snd.fst.nextElem none).getD 0) (p.snd.snd.fst.nextElem none) p.snd.snd.fst 0 p.snd.snd.snd.snd l bs fs parents

An internal off-path node initializes the same complete sweep contract, allowing the first child to settle a positive comparison.