theorem Hex.GraphIso.Nauty.Max.Loop.first_prepare {n : Nat} {ctx : Ctx n} {tcLevel : Nat} {l : Loop n} (hf : l.first = true) : prepare ctx tcLevel l = have r := Generic.prepareFirst ctx tcLevel l.node.level l.node.numcells l.node.entry; (r.fst, r.snd.fst, r.snd.snd.fst, r.snd.snd.snd.fst, cheapCheck true l.node.level r.snd.snd.snd.snd)

The frozen first sweep uses exactly the first-path preparation.

theorem Hex.GraphIso.Nauty.Max.SweepInput.child_entry {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel cfuel : Nat} {first : Bool} {level numcells tc tv1 tv index : Nat} {cell : VSet n} {st : Search n} {l : Loop n} {bs fs : List Nat} {parents : Parents n} (h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l 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) : Entry G ctx tcLevel (first && tv == tv1) { level := level + 1, numcells := numcells + 1, codes := Loop.codes ctx l, entry := child first level tc tv st } bs fs

Both sweep phases establish the actual child's first-path or off-path entry conditions, including its full stored code prefix.

theorem Hex.GraphIso.Nauty.Max.SweepInput.push {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel cfuel : Nat} {first : Bool} {level numcells tc tv1 tv index : Nat} {cell : VSet n} {st : Search n} {l : Loop n} {bs fs : List Nat} {parents : Parents n} (h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l 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) : have p := { loop := l, state := st, chosen := tv, bs := bs, fs := fs }; NodeInput G ctx tcLevel fuel (first && tv == tv1) (Parent.child ctx tcLevel p) bs fs (parents.push p)

Every actual visited child satisfies the complete maximum input. All ancestor facts are constructed from the suspended sweep.

theorem Hex.GraphIso.Nauty.Max.NodeInput.stored {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) (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) : RunInv G ctx (node first ctx (n + 2) tcLevel fuel f.level f.numcells f.entry).snd

Actual node calls establish the checked store needed by receiving filters, on both the first path and later sibling paths.