theorem Hex.GraphIso.Nauty.Sparse.State.invalidate_frame {n : Nat} (st : State n) : frame { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong.invalidate, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, order := st.order, genTrace := st.genTrace, workperm := st.workperm } = st.frame

Cache invalidation is invisible to the shared proof frame.

theorem Hex.GraphIso.Nauty.Sparse.State.child_frame {n : Nat} (first : Bool) (level tc tv : Nat) (st : State n) : (Generic.Policy.child first level tc tv st).frame = child first level tc tv st.frame

The sparse child performs the shared individualization on its frame.

theorem Hex.GraphIso.Nauty.Sparse.State.recover_frame {n : Nat} (inf level : Nat) (st : State n) : (Generic.Policy.recover inf level st).frame = recover inf level st.frame

Recovery changes the shared partition and controls exactly as in the common engine; invalidating native cache indices adds no frame change.