theorem Hex.GraphIso.Nauty.Sparse.traceFramePolicy {n k : Nat} (G : Sparse.Colored n k) {base cells : Nat} {root : State n} (hp : Ready G base cells root) (hn : 0 < n) (hb : 1 ≤ base) (tcLevel : Nat) : Generic.SoundPolicy (Graph.ofGraph G.graph) (n + 2) tcLevel (traceFrameContract G base root)

The native mutual recursion preserves reference containment and generator stabilization at a fixed suspended ancestor.

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.node {n k : Nat} {G : Sparse.Colored n k} {base cells level numcells : Nat} {root st : State n} (h : TraceFrame G base root st) (hp : Ready G base cells root) (hn : 0 < n) (hb : 1 ≤ base) (hlevel : base < level) (hi : NodeInv G level numcells st) (first : Bool) (tcLevel fuel : Nat) : TraceFrame G base root (Generic.node first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd

Every complete or truncated descendant call preserves a frozen ancestor's saved-reference cells and all accumulated generator stabilizers.

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.sweep {n k : Nat} {G : Sparse.Colored n k} {base cells level numcells : Nat} {root st : State n} (h : TraceFrame G base root st) (hp : Ready G base cells root) (hn : 0 < n) (hb : 1 ≤ base) (hlevel : base ≤ level) (hi : Ready G level numcells st) (first : Bool) (tcLevel fuel cfuel tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (ht : Generic.Target State.frame level tc cell st) (hv : ∀ (v : Nat), cursor = some v → cell.mem v = true) : TraceFrame G base root (Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd

Every complete sibling sweep retains the frozen ancestor invariant, including filtered targets, orbit skips and returns past the current caller.