theorem Hex.GraphIso.Nauty.Sparse.Limited.budgetPolicy {n : Nat} (g : Graph n) (inf tcLevel limit : Nat) : Generic.Preserve g inf tcLevel (Budget limit)

Every executed policy callback conserves admitted visits plus quota.

theorem Hex.GraphIso.Nauty.Sparse.Limited.node_budget {n limit : Nat} {s : State n} (h : Budget limit s) (g : Graph n) (inf tcLevel fuel level numcells : Nat) (first : Bool) : Budget limit (Generic.node first g inf tcLevel fuel level numcells s).snd

The actual mutual recursion conserves the quota through all returns.

theorem Hex.GraphIso.Nauty.Sparse.Limited.run?_budget {n limit : Nat} {g : Graph n} {lab : Array Nat} {ends : List Nat} {s : State n} (h : run? limit g lab ends = some s) : Budget limit s

Every accepted root retains its exact original node budget.

theorem Hex.GraphIso.Nauty.Sparse.Limited.run?_visited {n limit : Nat} {g : Graph n} {lab : Array Nat} {ends : List Nat} {s : State n} (h : run? limit g lab ends = some s) : s.visited ≤ limit

A successful bounded search never admits more than its node limit.

theorem Hex.GraphIso.Nauty.Sparse.Limited.runColored?_visited {n k limit : Nat} {G : Sparse.Colored n k} {s : State n} (h : runColored? limit G = some s) : s.visited ≤ limit

theorem Hex.GraphIso.Nauty.Sparse.Limited.frozenPolicy {n : Nat} (g : Graph n) (inf tcLevel : Nat) (s : State n) (hs : s.exhausted = true) : Generic.Preserve g inf tcLevel fun (t : State n) => t = s

After exhaustion every callback retains the entire wrapped state. The native payload cannot be changed by unwinding or sibling processing.

theorem Hex.GraphIso.Nauty.Sparse.Limited.node_exhausted {n : Nat} (g : Graph n) (inf tcLevel fuel level nc : Nat) (first : Bool) (s : State n) (hs : s.exhausted = true) : (Generic.node first g inf tcLevel fuel level nc s).snd = s

Exhaustion is absorbing throughout the actual mutual recursion.