theorem Hex.GraphIso.Nauty.FixedCells.fields {n level : Nat} {st out : Search n} (h : FixedCells level st) (hl : out.lab = st.lab) (hp : out.ptn = st.ptn) (hf : out.fixedpts = st.fixedpts) : FixedCells level out

Bookkeeping on other fields preserves the fixed singleton cells.

theorem Hex.GraphIso.Nauty.fixed_visit {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st : Search n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (h : FixedCells level st) : FixedCells level (visit ctx level numcells st).snd.snd

Refinement leaves every recorded fixed vertex in a singleton cell.

theorem Hex.GraphIso.Nauty.compare_fixed {n : Nat} {κ : Type} (level code : Nat) (st : SearchState n κ) : (compareCodes level code st).fixedpts = st.fixedpts

Comparison changes no fixed vertex or partition field.

theorem Hex.GraphIso.Nauty.target_fixed {n : Nat} (first : Bool) (ctx : Ctx n) (tcLevel level numcells : Nat) (st : Search n) : (chooseTarget first ctx tcLevel level numcells st).snd.snd.snd.fixedpts = st.fixedpts

Target selection changes no fixed vertex.

theorem Hex.GraphIso.Nauty.classify_fixed {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : (classify ctx level numcells st).snd.fixedpts = st.fixedpts

Classification fills scratch data without changing the fixed-point set.

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

Leaf actions leave the current individualized path unchanged.

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

The cheap-boundary test changes no fixed vertex.

theorem Hex.GraphIso.Nauty.recover_fixed {n : Nat} {κ : Type} (inf level : Nat) (st : SearchState n κ) : (recover inf level st).fixedpts = st.fixedpts

Partition recovery keeps the caller's fixed-point bitset.

theorem Hex.GraphIso.Nauty.afterSweep_fixed {n : Nat} {κ : Type} (first : Bool) (level size index : Nat) (st : SearchState n κ) : (afterSweep first level size index st).fixedpts = st.fixedpts

Sweep completion changes only counters.

theorem Hex.GraphIso.Nauty.fixed_child {n k : Nat} {G : Colored n k} {level numcells tc tv : Nat} {st : Search n} {cell : VSet n} (first : Bool) (hn0 : 0 < n) (hok : SearchOk G level numcells st) (h : FixedCells level st) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (htv : cell.mem tv = true) : st.fixedpts.mem tv = false ∧ FixedCells (level + 1) (child first level tc tv st)

An actual target vertex is fresh, and individualizing it extends the fixed singleton cells by exactly that vertex.

theorem Hex.GraphIso.Nauty.fixed_recover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st out : Search n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (h : FixedCells level st) (hout : SearchOut G level level st out) (hf : out.fixedpts = st.fixedpts) : FixedCells level (recover (n + 2) level out)

Recovering a completed child restores fixed singleton cells whenever the parent's fixed-point bitset has been restored.