theorem Hex.GraphIso.Nauty.Max.Loop.singleton {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel a : Nat} {l : Loop n} (h : Frame.Valid G l.node) (ha : IsCell l.node.entry.ptn l.node.level a 1) : IsCell (prepare ctx tcLevel l).snd.snd.snd.snd.ptn l.node.level a 1 ∧ (prepare ctx tcLevel l).snd.snd.snd.snd.lab[a]! = l.node.entry.lab[a]!

Preparing a node preserves its entry singletons and their vertices.

theorem Hex.GraphIso.Nauty.Max.Parent.picked {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {p : Parent n} (h : Valid G ctx tcLevel p) : have ch := child ctx tcLevel p; have tc := (Loop.prepare ctx tcLevel p.loop).snd.fst.toNat; IsCell ch.entry.ptn ch.level tc 1 ∧ ch.entry.lab[tc]! = p.chosen

A saved parent's selected vertex is a singleton at its actual child entry.

theorem Hex.GraphIso.Nauty.Max.Parent.singleton {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel a : Nat} {p : Parent n} (h : Valid G ctx tcLevel p) (ha : IsCell p.loop.node.entry.ptn p.loop.node.level a 1) : IsCell p.state.ptn p.loop.node.level a 1

A saved child singleton remains present when its node's sweep resumes.

theorem Hex.GraphIso.Nauty.Max.SweepInput.singletons {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel cfuel : Nat} {first : Bool} {level numcells tc tv1 index : Nat} {cursor : Option Nat} {cell : VSet n} {st : Search n} {l : Loop n} {bs fs : List Nat} {parents : Parents n} (h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 cursor cell index st l bs fs parents) {t : Nat} {p : Parent n} (hp : parents t = some p) : IsCell st.ptn level (Loop.prepare ctx tcLevel p.loop).snd.fst.toNat 1

The saved ancestor chain supplies every earlier selected singleton. No additional singleton invariant is required at the sweep entry.

theorem Hex.GraphIso.Nauty.Max.SweepInput.child_chosen {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel cfuel : Nat} {first : Bool} {level numcells tc tv1 tv index : Nat} {cell : VSet n} {st : Search n} {l : Loop n} {bs fs : List Nat} {parents : Parents n} (h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents) {t : Nat} {p : Parent n} (hp : parents t = some p) : (child first level tc tv st).lab[(Loop.prepare ctx tcLevel p.loop).snd.fst.toNat]! = p.chosen

Individualizing the next target preserves all earlier chosen vertices.

theorem Hex.GraphIso.Nauty.Max.extend_effect {n k : Nat} {G : Colored n k} {t level nc mc : Nat} {base st out : Search n} (ht : 1 ≤ t) (htl : t ≤ level) (hb : SearchOk G t nc base) (hs : SearchOk G level mc st) (he : SearchOut G t t base st) (ho : SearchOut G level level st out) : SearchOut G t t base out

A finer partition effect composes with a saved ancestor's effect, including references installed within the finer partition.