theorem
Hex.GraphIso.Nauty.Sparse.Ready.first_choice
{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).fst = Int.ofNat (targetcell (Graph.ofGraph G.graph) st.lab st.ptn level tcLevel (-1))
The real first-path target dispatch chooses the unhinted native target, using its established indexed scratch and nonempty partition.
theorem
Hex.GraphIso.Nauty.Sparse.prepareFirst_choice
{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)
(hopen : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).fst ≠ n)
:
(Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).snd.fst = Int.ofNat
(targetcell (Graph.ofGraph G.graph) (State.refined (Graph.ofGraph G.graph) level numcells st).lab
(State.refined (Graph.ofGraph G.graph) level numcells st).ptn level tcLevel (-1))
The mathematical target of the first descent is the actual cached refinement's native target, with no conversion to dense refinement.