theorem Hex.GraphIso.Nauty.Sparse.classify_open {n : Nat} {g : Graph n} {level numcells : Nat} {st : State n} (h : (classify g level numcells st).fst = Generic.Leaf.internal) : numcells ≠ n

theorem Hex.GraphIso.Nauty.Sparse.CheapRecorded.classified {n : Nat} {g : Graph n} {level numcells tc : Nat} {st : State n} (h : CheapRecorded level tc st) : have c := classify g level numcells st; CheapRecorded level tc (leafExit c.fst level c.snd).snd

Classification and leaf bookkeeping retain a recorded sweep target; only the later cheap guard can make that recording irrelevant.

theorem Hex.GraphIso.Nauty.Sparse.node_trace {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel fuel level numcells : Nat) (st : State n) : 1 ≤ level → TraceEntry G tcLevel level numcells st → TraceOk G (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd

Every complete or truncated off-path call preserves soundness of the literal emitted trace. The mutual node/sibling induction establishes all admission histories from the entry's pending native visit.