theorem Hex.GraphIso.Nauty.Sparse.targetcell_hint {n : Nat} (g : Graph n) (lab ptn : Array Nat) (level tcLevel : Nat) : targetcell g lab ptn level tcLevel (Int.ofNat (targetcell g lab ptn level tcLevel (-1))) = targetcell g lab ptn level tcLevel (-1)

Supplying the unhinted target as a hint leaves the target unchanged, whether the hint guard accepts it or dispatches to the unhinted rule.

theorem Hex.GraphIso.Nauty.Sparse.targetCached_hint {n : Nat} (G : SparseGraph n) (lab ptn : Array Nat) (level tcLevel : Nat) (s : Scratch) (l : Label n) (hl : Label.ofArray? n lab = some l) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hi : Scratch.Valid n lab ptn level s) (hc : bcount ptn level n < n) {hint : Int} (hh : Int.ofNat (targetcell (Graph.ofGraph G) lab ptn level tcLevel (-1)) = hint) : have a := maketargetCached (Graph.ofGraph G) lab ptn level tcLevel hint s; have b := maketargetCached (Graph.ofGraph G) lab ptn level tcLevel (-1) s; (a.fst, a.snd.fst, a.snd.snd.fst) = (b.fst, b.snd.fst, b.snd.snd.fst)

Cached hint dispatch retains the complete target position, vertex set and size when the hint agrees with the unhinted rule. Scratch may change.

theorem Hex.GraphIso.Nauty.Sparse.FirstRef.cached_target {n : Nat} {G : SparseGraph n} {tcLevel base level : Nat} {root current : RefineSt n} {st : State n} (h : FirstRef G tcLevel base root st) (hdepth : level ≤ h.last) (hr : RefineSt.Ready G base root) (hc : RefineSt.Ready G level current) (hshape : NodeShape n base root.ptn) (hp : FollowsPerm G st.firsttc base root level current) (hopen : discreteAt current.ptn level n ≠ true) (scratch : Scratch) (hs : Scratch.Valid n current.lab current.ptn level scratch) : have a := maketargetCached (Graph.ofGraph G) current.lab current.ptn level tcLevel st.firsttc[level]! scratch; have b := maketargetCached (Graph.ofGraph G) current.lab current.ptn level tcLevel (-1) scratch; (a.fst, a.snd.fst, a.snd.snd.fst) = (b.fst, b.snd.fst, b.snd.snd.fst)

The actual cached target fields agree with unhinted selection along a live history below a cheap ancestor, using the stored first target as hint.