theorem Hex.GraphIso.Nauty.Sparse.FrameOut.vertex_key {n k : Nat} {G : Sparse.Colored n k} {level numcells tc len v fuel tcLevel : Nat} {st out : State n} (h : FrameOut G level level st out) (hs : Ready G level numcells st) (ho : Ready G level numcells out) (hn : 0 < n) (hl : 1 ≤ level) (hc : IsCell st.ptn level tc len) (hlen : 1 < len) (hr : tc + len ≤ n) (hv : (windowSet n st.lab tc len).mem v = true) (hf : n < fuel + (numcells + 1)) : vertexKey G.graph tcLevel fuel level st.lab st.ptn tc numcells v = vertexKey G.graph tcLevel fuel level out.lab out.ptn tc numcells v

The actual recovered parent frame preserves the full unpruned key of every vertex-indexed child, despite changing its offset in the target cell.