theorem Hex.GraphIso.Nauty.Sparse.chooseTarget_codes {n : Nat} (first : Bool) (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : have out := (chooseTarget first g tcLevel level numcells st).snd.snd.snd; out.canoncode = st.canoncode ∧ out.canonlevel = st.canonlevel ∧ out.eqlevCanon = st.eqlevCanon ∧ out.compCanon = st.compCanon ∧ out.canonlab = st.canonlab ∧ out.firstlab = st.firstlab

Native target selection preserves canonical comparison storage and both reference labels, including when it borrows the cached scratch.

theorem Hex.GraphIso.Nauty.Sparse.prepareFirst_canoncode {n : Nat} (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : (Generic.prepareFirst g tcLevel level numcells st).snd.snd.snd.snd.canoncode = st.canoncode

First preparation leaves the preallocated incumbent code array intact.

theorem Hex.GraphIso.Nauty.Sparse.firstPath_canoncode {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.canoncode = st.canoncode

Every first-path descent reaches its leaf with the original canonical code allocation. Only leaf installation begins writing incumbent codes.