theorem Hex.GraphIso.Nauty.Sparse.classify_scratch {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) : (classify g level numcells st).snd.canong.scratch = st.canong.scratch

Sparse leaf classification may update canonical rows and scatter a permutation, but retains the independent refinement scratch exactly.

theorem Hex.GraphIso.Nauty.Sparse.boundsPolicy {n : Nat} (g : Graph n) (inf tcLevel : Nat) : Generic.Preserve g inf tcLevel fun (st : State n) => Scratch.Bounded n st.canong.scratch

Every actual sparse policy operation preserves persistent allocations and mark bounds. No partition-validity or recursive-correctness premise is needed.

theorem Hex.GraphIso.Nauty.Sparse.node_bounded {n : Nat} (g : Graph n) (first : Bool) (inf tcLevel fuel level numcells : Nat) (st : State n) (h : Scratch.Bounded n st.canong.scratch) : Scratch.Bounded n (Generic.node first g inf tcLevel fuel level numcells st).snd.canong.scratch

The real production node preserves scratch bounds on first and later paths, for every fuel value and every kind of return.

theorem Hex.GraphIso.Nauty.Sparse.sweep_bounded {n : Nat} (g : Graph n) (first : Bool) (inf tcLevel fuel cfuel level numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : State n) (h : Scratch.Bounded n st.canong.scratch) : Scratch.Bounded n (Generic.sweep first g inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.canong.scratch

theorem Hex.GraphIso.Nauty.Sparse.run_bounded {n : Nat} (g : Graph n) (lab : Array Nat) (ends : List Nat) : Scratch.Bounded n (run g lab ends).canong.scratch

Root initialization establishes the invariant, so production execution needs no external scratch hypothesis. Finishing canonical rows retains it.