structure Hex.GraphIso.Nauty.RunInv {n k : Nat} (G : Colored n k) (ctx : Ctx n) (st : Search n) : Prop

Persistent state after the first leaf. Partition frames and their conditional descent histories belong to the individual call contract.

• first : st.firstlab.toList.Perm (List.range n)
• canonical : st.canonlab.size = n ∧ CellsReach G st.canonlab
• cache : CanongInv ctx st.canong st.canonlab st.samerows
• scratch : st.workperm.size = n
• trace : TraceOk ctx st
• orbits : OrbitsOk st

  Every orbit pointer is connected by recorded generators.

• firstReach : CellsReach G st.firstlab

  The saved first labelling respects the initial colour cells.

• colors : TraceStab G st

  Recorded generators stabilize the initial colour partition.

• pairs : PairsOk G ctx st

  Every pruning pair has checked colour-preserving realizers.

• workspace : WorkspaceOk st

theorem Hex.GraphIso.Nauty.RunInv.firstSize {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} (h : RunInv G ctx st) : st.firstlab.size = n

The saved first permutation has exactly one entry for every vertex.

theorem Hex.GraphIso.Nauty.RunInv.of_out {n k : Nat} {G : Colored n k} {ctx : Ctx n} {B level : Nat} {st out : Search n} (h : RunInv G ctx st) (hout : SearchOut G B level st out) (hfirst : out.firstlab = st.firstlab) (hcache : CanongInv ctx out.canong out.canonlab out.samerows) (hscratch : out.workperm.size = st.workperm.size) (htrace : TraceOk ctx out) (horbits : OrbitsOk out) (hcolors : TraceStab G out) (hpairs : PairsOk G ctx out) (hworkspace : WorkspaceOk out) : RunInv G ctx out

Frame receipts preserve the installed canonical labelling; reference, cache and scratch facts assemble the persistent invariant at a return.

theorem Hex.GraphIso.Nauty.RunInv.congr {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st out : Search n} (h : RunInv G ctx st) (hf : out.firstlab = st.firstlab) (hc : out.canonlab = st.canonlab) (hstore : CanongInv ctx out.canong out.canonlab out.samerows) (hw : out.workperm.size = st.workperm.size) (ht : out.genTrace = st.genTrace) (ho : out.orbits = st.orbits) (ha : out.autos = st.autos) (hcap : out.wsCap = st.wsCap) : RunInv G ctx out

Equal persistent fields retain the invariant during local bookkeeping.

theorem Hex.GraphIso.Nauty.RunInv.visit {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} (h : RunInv G ctx st) (level numcells : Nat) : RunInv G ctx (Nauty.visit ctx level numcells st).snd.snd

Node refinement preserves the persistent state.

theorem Hex.GraphIso.Nauty.RunInv.compare {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} (h : RunInv G ctx st) (level code : Nat) : RunInv G ctx (compareCodes level code st)

Code comparison changes only comparison counters and the in-progress canonical codes.

theorem Hex.GraphIso.Nauty.RunInv.target {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} (h : RunInv G ctx st) (tcLevel level numcells : Nat) : RunInv G ctx (chooseTarget false ctx tcLevel level numcells st).snd.snd.snd

Off-path target selection preserves the persistent state.

theorem Hex.GraphIso.Nauty.RunInv.classify {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} (h : RunInv G ctx st) (level numcells : Nat) : RunInv G ctx (Nauty.classify ctx level numcells st).snd

Classification updates the canonical row cache and retains the persistent state.

theorem Hex.GraphIso.Nauty.RunInv.leaf {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells : Nat} {st : Search n} (h : RunInv G ctx st) (leaf : Leaf) (hok : SearchOk G level numcells st) (hnew : ∀ (sr : Nat), leaf = Generic.Leaf.better sr → CanongInv ctx st.canong st.lab sr) (hcheck : leaf = Generic.Leaf.autoFirst ∨ leaf = Generic.Leaf.autoCanon → checkAutom ctx.g st.workperm = true) (hcolor : leaf = Generic.Leaf.autoFirst ∨ leaf = Generic.Leaf.autoCanon → ColorStab G st.workperm) (hn0 : 0 < n) (hboundary : Boundary G ctx level st) (hbound : st.noncheaplevel ≤ level) : RunInv G ctx (leafExit leaf level st).snd

Acting on a classification preserves the persistent state once admissions are checked.

theorem Hex.GraphIso.Nauty.RunInv.cheap {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} (h : RunInv G ctx st) (first : Bool) (level : Nat) : RunInv G ctx (cheapCheck first level st)

The cheap-boundary update preserves persistent data.

theorem Hex.GraphIso.Nauty.RunInv.child {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} (h : RunInv G ctx st) (first : Bool) (level tc tv : Nat) : RunInv G ctx (Nauty.child first level tc tv st)

Individualizing a vertex changes no saved leaf or generator data.

theorem Hex.GraphIso.Nauty.RunInv.leave {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} (h : RunInv G ctx st) (tv : Nat) : RunInv G ctx { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts.erase tv, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, 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 }

Removing the temporary fixed point preserves persistent data.

theorem Hex.GraphIso.Nauty.RunInv.recover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} (h : RunInv G ctx st) (inf level : Nat) : RunInv G ctx (Nauty.recover inf level st)

Recovering the parent partition does not alter saved leaves or generator data.

theorem Hex.GraphIso.Nauty.RunInv.afterSweep {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} (h : RunInv G ctx st) (first : Bool) (level size index : Nat) : RunInv G ctx (Nauty.afterSweep first level size index st)

Completing a sweep changes only its symmetry counter.