theorem Hex.GraphIso.Nauty.Sparse.target_empty {n : Nat} (level tc : Nat) (st : State n) : Generic.Target State.frame level tc VSet.empty st

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

A fresh native target denotes exactly a bounded nontrivial partition cell, with each selected vertex drawn from its current labels.

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

The cached target supplies the identical cell-membership contract using the proved fresh/cached dispatch equality and a constructed parsed label.

theorem Hex.GraphIso.Nauty.Sparse.Ready.target {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (first : Bool) (tcLevel : Nat) : have t := chooseTarget first (Graph.ofGraph G.graph) tcLevel level numcells st; Generic.Target State.frame level t.fst.toNat t.snd.fst t.snd.snd.snd

The actual target-selection guards produce either an empty target or a nontrivial current cell. Both first and hinted off-path dispatches are covered.