theorem Hex.GraphIso.Nauty.Sparse.chooseTarget_trace {n : Nat} (first : Bool) (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : (chooseTarget first g tcLevel level numcells st).snd.snd.snd.genTrace = st.genTrace

Native target selection never removes an emitted generator.

theorem Hex.GraphIso.Nauty.Sparse.tracePolicy {n : Nat} (g : Graph n) (inf tcLevel : Nat) (gamma : Array Nat) : Generic.Preserve g inf tcLevel fun (st : State n) => gamma ∈ st.genTrace

Every literal policy transition retains each previously emitted array, including the first descent, first-child bookkeeping and recovery.

theorem Hex.GraphIso.Nauty.Sparse.node_contains {n : Nat} (first : Bool) (g : Graph n) (inf tcLevel fuel level numcells : Nat) (st : State n) {gamma : Array Nat} (h : gamma ∈ st.genTrace) : gamma ∈ (Generic.node first g inf tcLevel fuel level numcells st).snd.genTrace

Both complete native node calls retain their incoming trace, even when fuel expires or a return crosses multiple suspended parents.

theorem Hex.GraphIso.Nauty.Sparse.sweep_contains {n : Nat} (first : Bool) (g : Graph n) (inf tcLevel fuel cfuel level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : State n) {gamma : Array Nat} (h : gamma ∈ st.genTrace) : gamma ∈ (Generic.sweep first g inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.genTrace

A native sibling continuation retains every generator already received from a child, irrespective of its first-sweep flag.