theorem Hex.GraphIso.Nauty.Sparse.Target.nonempty {n level : Nat} {ptn : Array Nat} (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hc : bcount ptn level n < n) : nontrivial (cells ptn level n) ≠ []

A valid partition with fewer than n cells has a nontrivial cell.

theorem Hex.GraphIso.Nauty.Sparse.targetcell_nontrivial {n : Nat} (G : SparseGraph n) (lab ptn : Array Nat) (level tcLevel : Nat) (hint : Int) (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hc : bcount ptn level n < n) : targetcell (Graph.ofGraph G) lab ptn level tcLevel hint ∈ Target.nontrivial (cells ptn level n)

Fresh target selection needs no caller-supplied label parser success or cache: both are derived from the node's permutation and partition facts.

theorem Hex.GraphIso.Nauty.Sparse.maketargetcell_valid {n : Nat} (G : SparseGraph n) (lab ptn : Array Nat) (level tcLevel : Nat) (hint : Int) (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hc : bcount ptn level n < n) : have t := maketargetcell (Graph.ofGraph G) lab ptn level tcLevel hint; IsCell ptn level t.fst t.snd.snd ∧ 1 < t.snd.snd ∧ t.fst + t.snd.snd ≤ n

The fresh target's returned size is the length of a bounded nontrivial partition cell, including valid hints and both depth-cutoff branches.

theorem Hex.GraphIso.Nauty.Sparse.maketargetCached_validCell {n : Nat} (G : SparseGraph n) (lab ptn : Array Nat) (level tcLevel : Nat) (hint : Int) (scratch : Scratch) (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hv : Scratch.Valid n lab ptn level scratch) (hc : bcount ptn level n < n) : have t := maketargetCached (Graph.ofGraph G) lab ptn level tcLevel hint scratch; IsCell ptn level t.fst t.snd.snd.fst ∧ 1 < t.snd.snd.fst ∧ t.fst + t.snd.snd.fst ≤ n

Every admissible scratch state yields the same bounded nontrivial target as the fresh selector, without additional cache or parsing assumptions.