theorem Hex.GraphIso.Nauty.Sparse.chooseTarget_orbits {n : Nat} (first : Bool) (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : (chooseTarget first g tcLevel level numcells st).snd.snd.snd.orbits = st.orbits

Borrowing target scratch and saving the first target leaves the orbit array untouched. This concerns the native sparse dispatch.

theorem Hex.GraphIso.Nauty.Sparse.prepareFirst_orbits {n : Nat} (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : (Generic.prepareFirst g tcLevel level numcells st).snd.snd.snd.snd.orbits = st.orbits

theorem Hex.GraphIso.Nauty.Sparse.Ready.first_nonempty {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hc : numcells < n) : (chooseTarget true (Graph.ofGraph G.graph) tcLevel level numcells st).snd.fst ≠ VSet.empty

Every open first-path target contains a current vertex. The cache agreement theorem supplies the exact workset used by the executable.

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

Preparation establishes an equitable parent and the actual target's membership contract, starting with the production entry invariant.