theorem
Hex.GraphIso.Nauty.Sparse.Ready.match_target
{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)
(heq : st.eqlevFirst = level)
(hslot : st.firsttc[level]! = Int.ofNat (targetcell (Graph.ofGraph G.graph) st.lab st.ptn level tcLevel (-1)))
:
A stored target equal to the unhinted native rule survives both cached dispatch arms, including a changed scratch result.