theorem Hex.GraphIso.Nauty.Sparse.boundaryPolicy {n : Nat} (g : Graph n) (inf tcLevel bound saved : Nat) : Generic.BoundedPolicy g inf tcLevel bound fun (st : State n) => st.noncheaplevel = saved ∨ bound < st.noncheaplevel

A saved cheap boundary above the receiving ancestor is either retained literally or replaced strictly below that ancestor by the actual sparse policy.

theorem Hex.GraphIso.Nauty.Sparse.node_boundary {n : Nat} (g : Graph n) (inf tcLevel fuel level numcells : Nat) (st : State n) (hl : 0 < level) : (Generic.node false g inf tcLevel fuel level numcells st).snd.noncheaplevel = st.noncheaplevel ∨ level ≤ (Generic.node false g inf tcLevel fuel level numcells st).snd.noncheaplevel

An off-path native call can change an older cheap boundary only at or below its own depth, including truncated calls and nonlocal returns.