theorem Hex.GraphIso.Nauty.Sparse.Max.NodeInput.prepare {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : NodeInput G tcLevel f bs fs parents) (hi : have p := prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry; (classify (Graph.ofGraph G.graph) f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.internal) : have l := { node := f, first := false }; have p := Loop.prepare G.graph tcLevel l; SweepInput G tcLevel l bs fs (p.snd.snd.fst.nextElem none) p.snd.snd.fst p.snd.snd.snd.snd parents

An internal off-path node establishes the complete initial sweep context from its literal native preparation. The selected bitset is the whole frozen cell, so ranked coverage starts with every child live.