theorem Hex.GraphIso.Nauty.Sparse.chooseFirst_store {n : Nat} (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : have r := chooseTarget true g tcLevel level numcells st; r.snd.snd.snd.firstcode = st.firstcode ∧ r.snd.snd.snd.firsttc = st.firsttc.set! level r.fst

First-path target selection writes exactly its current target slot, while retaining the code array. Scratch borrowing does not affect either.

theorem Hex.GraphIso.Nauty.Sparse.prepareFirst_store {n : Nat} (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : have r := Generic.prepareFirst g tcLevel level numcells st; r.snd.snd.snd.snd.firstcode = st.firstcode.set! level (visit g level numcells st).snd.fst ∧ r.snd.snd.snd.snd.firsttc = st.firsttc.set! level r.snd.fst

Preparation records the actual cached refinement code and native target in their depth-indexed slots.

theorem Hex.GraphIso.Nauty.Sparse.firstPath_storeSize {n : Nat} {g : Graph n} {tcLevel fuel level numcells last : Nat} {st leaf : State n} (path : Generic.FirstPath g tcLevel fuel level numcells st last leaf) : (leaf.firstcode.size, leaf.firsttc.size) = (st.firstcode.size, st.firsttc.size)

The actual first descent retains both reference-array allocations.

theorem Hex.GraphIso.Nauty.Sparse.firstPath_before {n : Nat} {g : Graph n} {tcLevel fuel level numcells last slot : Nat} {st leaf : State n} (path : Generic.FirstPath g tcLevel fuel level numcells st last leaf) (hs : slot < level) : (leaf.firstcode[slot]!, leaf.firsttc[slot]!) = (st.firstcode[slot]!, st.firsttc[slot]!)

A deeper first-path visit preserves both code and target entries of every earlier ancestor.

theorem Hex.GraphIso.Nauty.Sparse.firstPath_sentinel {n : Nat} {g : Graph n} {inf tcLevel fuel level numcells last : Nat} {st leaf : State n} (path : Generic.FirstPath g tcLevel fuel level numcells st last leaf) (hs : last + 1 < st.firstcode.size) : (Generic.node true g inf tcLevel fuel level numcells st).snd.firstcode[last + 1]! = codeSentinel

The sentinel installed immediately below the actual first leaf survives the complete search, at the unchanged allocated position.