theorem
Hex.GraphIso.Nauty.Sparse.chooseTarget_fields
{n : Nat}
{g : Graph n}
{tcLevel level numcells : Nat}
{st : State n}
(first : Bool)
(hc : numcells < n)
(ho : first = true ∨ st.eqlevFirst = level ∨ 0 ≤ st.compCanon)
:
have t := chooseTarget first g tcLevel level numcells st;
have hint := if (!first && decide (st.compCanon < 0)) = true then st.firsttc[level]! else -1;
have c := maketargetCached g st.lab st.ptn level tcLevel hint st.canong.scratch;
(t.fst.toNat, t.snd.fst, t.snd.snd.fst) = (c.fst, c.snd.fst, c.snd.snd.fst)
An enabled native target dispatch returns all three fields of its actual cached selection, including the saved hint in a negative branch.
theorem
Hex.GraphIso.Nauty.Sparse.Ready.selected_cell
{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)
(first : Bool)
(ho : first = true ∨ st.eqlevFirst = level ∨ 0 ≤ st.compCanon)
:
Every enabled cached selection is exactly a complete nonsingleton window of the actual equitable parent, even when the target is hinted.
theorem
Hex.GraphIso.Nauty.Sparse.chooseTarget_open
{n : Nat}
{g : Graph n}
{tcLevel level numcells : Nat}
{st : State n}
(hi :
(classify g level numcells (chooseTarget false g tcLevel level numcells st).snd.snd.snd).fst = Generic.Leaf.internal)
:
An internal classification after target selection certifies that the selection guard was enabled. A disabled guard leaves the rejected code and first-reference level unchanged and is classified as bad.