def Hex.GraphIso.Nauty.FixedCells {n : Nat} (level : Nat) (st : Search n) : Prop

Every vertex recorded as fixed occupies a singleton cell of the current partition. This is the executable path fact that makes erasing a completed child's temporary fixed vertex restore its parent set exactly.

Equations

• Hex.GraphIso.Nauty.FixedCells level st = ∀ (v : Nat), v < n → st.fixedpts.mem v = true → ∃ (q : Nat), q < n ∧ st.lab[q]! = v ∧ Hex.GraphIso.Nauty.IsCell st.ptn level q 1

theorem Hex.GraphIso.Nauty.FixedCells.fresh {n level tc len o : Nat} {st : Search n} (h : FixedCells level st) (hok : LabOk st.lab n) (hinj : LabInj st.lab n) (hsize : st.lab.size = n) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) : st.fixedpts.mem st.lab[tc + o]! = false

A vertex in a non-singleton target cell is not already fixed.

theorem Hex.GraphIso.Nauty.FixedCells.ofCellsPerm {n level : Nat} {st out : Search n} (h : FixedCells level st) (hfixed : out.fixedpts = st.fixedpts) (hptn : out.ptn = st.ptn) (hperm : cellsPerm st.ptn level st.lab out.lab) : FixedCells level out

Reordering vertices within unchanged cells preserves fixed singletons.

theorem Hex.GraphIso.Nauty.FixedCells.ofEffect {n k : Nat} {G : Colored n k} {level : Nat} {st out : Search n} (h : FixedCells level st) (hfixed : out.fixedpts = st.fixedpts) (heffect : SearchOut G level level st out) : FixedCells level out

A parent-level search effect preserves fixed singletons when it preserves the fixed-point bitset.

theorem Hex.GraphIso.Nauty.FixedCells.fmptn {n level saved : Nat} {st : Search n} (h : FixedCells level st) (hsize : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hsaved : level ≤ saved) : st.fixedpts.subset (Nauty.fmptn st.lab st.ptn saved n).fst = true

Fixed singleton cells are present in the implicit pair at every deeper comparison level.

theorem Hex.GraphIso.Nauty.FixedCells.ofSearchOut {n k : Nat} {G : Colored n k} {level numcells : Nat} {st out : Search n} (h : FixedCells level st) (hfixed : out.fixedpts = st.fixedpts) (_hok : SearchOk G level numcells st) (_hout : SearchOk G level numcells out) (heffect : SearchOut G level level st out) : FixedCells level out

A parent-level search effect preserves fixed singletons between valid partition states.

theorem Hex.GraphIso.Nauty.FixedCells.refine {n : Nat} {ctx : Ctx n} {level : Nat} {active : VSet n} {numcells : Nat} {st : Search n} (h : FixedCells level st) (hsize : st.lab.size = n) (hpsize : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) : FixedCells level { lab := (Nauty.refine ctx level st.lab st.ptn active numcells).lab, ptn := (Nauty.refine ctx level st.lab st.ptn active numcells).ptn, active := (Nauty.refine ctx level st.lab st.ptn active numcells).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, 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 }

Refinement preserves every existing fixed singleton.

theorem Hex.GraphIso.Nauty.FixedCells.breakout {n level tc len o : Nat} {st : Search n} (h : FixedCells level st) (hinj : LabInj st.lab n) (hsize : st.lab.size = n) (hpsize : st.ptn.size = n) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) : FixedCells (level + 1) { lab := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst, ptn := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.fst, active := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert st.lab[tc + o]!, 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 }

Individualizing a fresh target vertex adds exactly one fixed singleton and preserves every older fixed singleton.

theorem Hex.GraphIso.Nauty.fixTest_mono {n : Nat} {small large fix : VSet n} (hsub : ∀ (v : Nat), small.mem v = true → large.mem v = true) (hfix : large.subset fix = true) : small.subset fix = true

Passing a fix test for a larger fixed set implies passing it for any pointwise smaller set.

def Hex.GraphIso.Nauty.LocalAutos {n : Nat} (ctx : Ctx n) (level : Nat) (st : Search n) : Prop

The bounded automorphism workspace is valid at the current frame for every entry whose fixed set covers the current search path.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.LocalAutos.empty {n : Nat} {ctx : Ctx n} {level : Nat} {st : Search n} (h : st.autos = #[]) : LocalAutos ctx level st

An empty workspace is locally valid.

theorem Hex.GraphIso.Nauty.LocalAutos.reindexStab {ptn lab lab' gamma : Array Nat} {level n : Nat} (h : CellStab ptn level lab gamma) (hperm : cellsPerm ptn level lab lab') (hpsize : ptn.size = n) (hsize : lab.size = n) (hsize' : lab'.size = n) (hend : ptn[ptn.size - 1]! ≤ level) : CellStab ptn level lab' gamma

Cell stabilization is independent of the ordering chosen inside each cell.

theorem Hex.GraphIso.Nauty.LocalAutos.reindexPair {n : Nat} {ctx : Ctx n} {ptn lab lab' : Array Nat} {level : Nat} {fix mcr : VSet n} (h : PairOk ctx.g ptn lab level fix mcr) (hperm : cellsPerm ptn level lab lab') (hpsize : ptn.size = n) (hsize : lab.size = n) (hsize' : lab'.size = n) (hend : ptn[ptn.size - 1]! ≤ level) : PairOk ctx.g ptn lab' level fix mcr

A locally valid pair remains valid after reordering the frame within its cells.

theorem Hex.GraphIso.Nauty.LocalAutos.ofCellsPerm {n : Nat} {ctx : Ctx n} {level : Nat} {st out : Search n} (h : LocalAutos ctx level st) (hautos : out.autos = st.autos) (hfixed : out.fixedpts = st.fixedpts) (hptn : out.ptn = st.ptn) (hperm : cellsPerm st.ptn level st.lab out.lab) (hpsize : st.ptn.size = n) (hsize : st.lab.size = n) (hsize' : out.lab.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) : LocalAutos ctx level out

Local ledger validity transports across unchanged partition cells and a within-cell labelling permutation.

theorem Hex.GraphIso.Nauty.LocalAutos.breakout {n : Nat} {ctx : Ctx n} {level tc len o : Nat} {st : Search n} (h : LocalAutos ctx level st) (hcell : IsCell st.ptn level tc len) (hrange : tc + len ≤ st.ptn.size) (hsize : st.lab.size = st.ptn.size) (hlab : LabOk st.lab n) (ho : o < len) (hlen : 2 ≤ len) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), st.ptn[q]! ≠ level + 1) : LocalAutos ctx (level + 1) { lab := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst, ptn := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.fst, active := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert st.lab[tc + o]!, 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 }

The conditional local ledger descends through one individualization. A pair applicable to the enlarged fixed set fixes the selected vertex, exactly the premise needed by cellStab_breakout.

theorem Hex.GraphIso.Nauty.LocalAutos.refine {n : Nat} {ctx : Ctx n} {level : Nat} {active : VSet n} {numcells : Nat} {st : Search n} (h : LocalAutos ctx level st) (hgsz : ctx.g.size = n) (hsize : st.lab.size = n) (hlab : LabOk st.lab n) (hpsize : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hstarts : ∀ (v : Nat), active.mem v = true → v = 0 ∨ st.ptn[v - 1]! ≤ level) : LocalAutos ctx level { lab := (Nauty.refine ctx level st.lab st.ptn active numcells).lab, ptn := (Nauty.refine ctx level st.lab st.ptn active numcells).ptn, active := (Nauty.refine ctx level st.lab st.ptn active numcells).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, 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 }

The conditional local ledger is preserved by equitable refinement.

def Hex.GraphIso.Nauty.PathStab {n : Nat} (ctx : Ctx n) (rootPtn rootLab : Array Nat) (level : Nat) (st : Search n) : Prop

A root-stabilizing checked automorphism that fixes every vertex on the current individualized path stabilizes the current partition. Keeping the root frame explicit lets the existing root autos ledger supply the same witness at every pruning site.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.PathStab.same {n : Nat} {ctx : Ctx n} {st : Search n} : PathStab ctx st.ptn st.lab 1 st

A frame is its own path-stabilization seed.

theorem Hex.GraphIso.Nauty.PathStab.ofCellsPerm {n : Nat} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level : Nat} {st out : Search n} (h : PathStab ctx rootPtn rootLab level st) (hfixed : out.fixedpts = st.fixedpts) (hptn : out.ptn = st.ptn) (hperm : cellsPerm st.ptn level st.lab out.lab) (hpsize : st.ptn.size = n) (hsize : st.lab.size = n) (hsize' : out.lab.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) : PathStab ctx rootPtn rootLab level out

Reordering the current labelling within unchanged cells preserves path stabilization.

theorem Hex.GraphIso.Nauty.PathStab.ofSearchOut {n k : Nat} {G : Colored n k} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level numcells : Nat} {st out : Search n} (h : PathStab ctx rootPtn rootLab level st) (hfixed : out.fixedpts = st.fixedpts) (hok : SearchOk G level numcells st) (hout : SearchOk G level numcells out) (heffect : SearchOut G level level st out) (hend : st.ptn[st.ptn.size - 1]! ≤ level) : PathStab ctx rootPtn rootLab level out

A parent-level search effect preserves path stabilization when it restores the parent's fixed-point set.

theorem Hex.GraphIso.Nauty.PathStab.refine {n : Nat} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level : Nat} {active : VSet n} {numcells : Nat} {st : Search n} (h : PathStab ctx rootPtn rootLab level st) (hgsz : ctx.g.size = n) (hsize : st.lab.size = n) (hlab : LabOk st.lab n) (hpsize : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hstarts : ∀ (v : Nat), active.mem v = true → v = 0 ∨ st.ptn[v - 1]! ≤ level) : PathStab ctx rootPtn rootLab level { lab := (Nauty.refine ctx level st.lab st.ptn active numcells).lab, ptn := (Nauty.refine ctx level st.lab st.ptn active numcells).ptn, active := (Nauty.refine ctx level st.lab st.ptn active numcells).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, 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 }

Equitable refinement preserves path stabilization.

theorem Hex.GraphIso.Nauty.PathStab.breakout {n : Nat} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level tc len o : Nat} {st : Search n} (h : PathStab ctx rootPtn rootLab level st) (hcell : IsCell st.ptn level tc len) (hrange : tc + len ≤ st.ptn.size) (hsize : st.lab.size = st.ptn.size) (hlab : LabOk st.lab n) (ho : o < len) (hlen : 2 ≤ len) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), st.ptn[q]! ≠ level + 1) : PathStab ctx rootPtn rootLab (level + 1) { lab := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst, ptn := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.fst, active := (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert st.lab[tc + o]!, 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 }

Individualization extends path stabilization because an automorphism fixing the enlarged path fixes the selected target vertex.

theorem Hex.GraphIso.Nauty.PathStab.toLocal {n : Nat} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level : Nat} {st : Search n} (h : PathStab ctx rootPtn rootLab level st) (hroot : AutosOk ctx.g rootPtn rootLab 1 st.autos) : LocalAutos ctx level st

The root autos ledger and path stabilization reconstruct the conditional ledger consumed by the two pruning filters.

structure Hex.GraphIso.Nauty.PathOk {n : Nat} (ctx : Ctx n) (rootPtn rootLab : Array Nat) (level : Nat) (st : Search n) : Prop

The two path facts carried by the mutual induction: fixed vertices are singleton cells, and root-valid automorphisms fixing them stabilize the current cells.

• fixed : FixedCells level st
• stab : PathStab ctx rootPtn rootLab level st

theorem Hex.GraphIso.Nauty.PathOk.refine {n k : Nat} {G : Colored n k} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level : Nat} {active : VSet n} {numcells : Nat} {st : Search n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hgsz : ctx.g.size = n) (hok : SearchOk G level numcells st) (hstarts : ∀ (v : Nat), active.mem v = true → v = 0 ∨ st.ptn[v - 1]! ≤ level) (h : PathOk ctx rootPtn rootLab level st) : PathOk ctx rootPtn rootLab level { lab := (Nauty.refine ctx level st.lab st.ptn active numcells).lab, ptn := (Nauty.refine ctx level st.lab st.ptn active numcells).ptn, active := (Nauty.refine ctx level st.lab st.ptn active numcells).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, 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 }

Node-entry refinement preserves both path facts.

theorem Hex.GraphIso.Nauty.PathOk.ofSearchOut {n k : Nat} {G : Colored n k} {ctx : Ctx n} {rootPtn rootLab : Array Nat} {level numcells : Nat} {st out : Search n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (h : PathOk ctx rootPtn rootLab level st) (hfixed : out.fixedpts = st.fixedpts) (hok : SearchOk G level numcells st) (hout : SearchOk G level numcells out) (heffect : SearchOut G level level st out) : PathOk ctx rootPtn rootLab level out

Recovered parent state preserves both path facts once child cleanup restores the parent's fixed-point set.