theorem Hex.GraphIso.Nauty.Max.Frame.first_step {n : Nat} {ctx : Ctx n} {tcLevel : Nat} {f : Frame n} (next : Generic.SweepFn (Search n) n) (hn : (Generic.prepareFirst ctx tcLevel f.level f.numcells f.entry).fst = n) : Generic.nodeStep ctx tcLevel next true f.level f.numcells f.entry = (Generic.Exit.unwind (f.level - 1) false, firstterminal f.level (Generic.prepareFirst ctx tcLevel f.level f.numcells f.entry).snd.snd.snd.snd)

A discrete first node installs its prepared leaf without a sweep.

theorem Hex.GraphIso.Nauty.Max.NodeInput.internal_keeps {n k : Nat} {G : Colored n k} {tcLevel fuel : Nat} {first : Bool} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : NodeInput G { g := rowsOf G } tcLevel (fuel + 1) first f bs fs parents) (hs : (contract G tcLevel).sweepValid fuel (n + 1) (Generic.sweepCall { g := rowsOf G } (n + 2) tcLevel fuel (n + 1))) (hfirst : first = true → (Generic.prepareFirst { g := rowsOf G } tcLevel f.level f.numcells f.entry).fst ≠ n) (hother : first = false → have p := prepareOther { g := rowsOf G } tcLevel f.level f.numcells f.entry; (classify { g := rowsOf G } f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.internal) : have ctx := { g := rowsOf G }; have result := Generic.nodeStep ctx tcLevel (Generic.sweepCall ctx (n + 2) tcLevel fuel (n + 1)) first f.level f.numcells f.entry; Keeps parents result.fst result.snd

An internal node transports the entire suffix trace through its ordinary completion or unchanged nonlocal exit.

theorem Hex.GraphIso.Nauty.Max.node_trace {n k : Nat} (G : Colored n k) (tcLevel : Nat) : NodeTraceRule G tcLevel

Every node preserves accumulated generators at surviving first ancestors, using the same smaller sweep contract as its key bounds.