theorem Hex.GraphIso.Nauty.Sparse.fixed_visit {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : NodeInv G level numcells st) (hf : FixedCells level st.frame) : FixedCells level (visit (Graph.ofGraph G.graph) level numcells st).snd.snd.frame

Native refinement retains the literal position of every fixed singleton and both of its old boundaries.

theorem Hex.GraphIso.Nauty.Sparse.compare_fixed {n : Nat} (level code : Nat) (st : State n) : (compareCodes level code st).fixedpts = st.fixedpts

theorem Hex.GraphIso.Nauty.Sparse.target_fixed {n : Nat} (first : Bool) (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : (chooseTarget first g tcLevel level numcells st).snd.snd.snd.fixedpts = st.fixedpts

Actual cached target selection leaves the individualized path unchanged.

theorem Hex.GraphIso.Nauty.Sparse.classify_fixed {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) : (classify g level numcells st).snd.fixedpts = st.fixedpts

theorem Hex.GraphIso.Nauty.Sparse.leaf_fixed {n : Nat} (leaf : Leaf) (level : Nat) (st : State n) : (leafExit leaf level st).snd.fixedpts = st.fixedpts

theorem Hex.GraphIso.Nauty.Sparse.cheap_fixed {n : Nat} (first : Bool) (level : Nat) (st : State n) : (cheapCheck first level st).fixedpts = st.fixedpts

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

theorem Hex.GraphIso.Nauty.Sparse.afterSweep_fixed {n : Nat} (first : Bool) (level size index : Nat) (st : State n) : (Generic.Policy.afterSweep first level size index st).fixedpts = st.fixedpts

theorem Hex.GraphIso.Nauty.Sparse.fixed_child {n k : Nat} {G : Sparse.Colored n k} {level numcells tc tv : Nat} {st : State n} {cell : VSet n} (first : Bool) (hn : 0 < n) (h : Ready G level numcells st) (hf : FixedCells level st.frame) (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) : st.fixedpts.mem tv = false ∧ FixedCells (level + 1) (Generic.Policy.child first level tc tv st).frame

Actual sparse child entry adds a fresh fixed vertex in a singleton cell. The native cache invalidation does not affect that path fact.

theorem Hex.GraphIso.Nauty.Sparse.fixed_recover {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st out : State n} (hn : 0 < n) (hl : 1 ≤ level) (h : Ready G level numcells st) (hf : FixedCells level st.frame) (hx : FrameOut G level level st out) (he : out.fixedpts = st.fixedpts) : FixedCells level (Generic.Policy.recover (n + 2) level out).frame

Recovering a returned child's partition preserves all parent fixed singletons once its temporary fixed vertex has been removed.

theorem Hex.GraphIso.Nauty.Sparse.fixed_restore {n tv : Nat} {st out : State n} (he : out.fixedpts = st.fixedpts.insert tv) (hf : st.fixedpts.mem tv = false) : out.fixedpts.erase tv = st.fixedpts

Removing the fresh child's fixed vertex restores the parent's bitset.