theorem
Hex.GraphIso.Nauty.Sparse.chooseTarget_pos
{n : Nat}
{g : Graph n}
{tcLevel level numcells : Nat}
{st : State n}
(hnc : numcells < n)
(he : st.eqlevFirst = level)
:
First-code agreement at an open node executes the cached target call with precisely the production hint, and returns its natural position.
theorem
Hex.GraphIso.Nauty.Sparse.chooseTarget_cast
{n : Nat}
{g : Graph n}
{tcLevel level numcells : Nat}
{st : State n}
(hnc : numcells < n)
(he : st.eqlevFirst = level)
:
Int.ofNat (chooseTarget false g tcLevel level numcells st).fst.toNat = (chooseTarget false g tcLevel level numcells st).fst
theorem
Hex.GraphIso.Nauty.Sparse.DescentAt.target
{n : Nat}
{G : SparseGraph n}
{tcLevel base level numcells : Nat}
{root : RefineSt n}
{st : State n}
(h : DescentAt G st.firsttc base root level numcells st)
(href : FirstRef G tcLevel base root st)
(hd : Depth href.last st)
(he : st.eqlevFirst = level)
(hnc : numcells < n)
(hr : RefineSt.Ready G base root)
(hshape : NodeShape n base root.ptn)
(hs : Scratch.Valid n st.lab st.ptn level st.canong.scratch)
:
The native frozen descent identifies the actual target with its saved slot, through both the hinted and ordinary cached dispatch arms.
theorem
Hex.GraphIso.Nauty.Sparse.Aligned.target_eq
{n : Nat}
{G : SparseGraph n}
{tcLevel base level numcells : Nat}
{root : RefineSt n}
{st : State n}
(h : Aligned G base root level level numcells st)
(href : FirstRef G tcLevel base root st)
(hd : Depth href.last st)
(hkeep : (chooseTarget false (Graph.ofGraph G) tcLevel level numcells st).snd.snd.snd.eqlevFirst = level)
(hnc : numcells < n)
(hr : RefineSt.Ready G base root)
(hshape : NodeShape n base root.ptn)
(hs : Scratch.Valid n st.lab st.ptn level st.canong.scratch)
:
A surviving first-target comparison agrees with the saved target. All descent and cache premises concern the actual native partition.