structure Hex.GraphIso.Nauty.CheapOk {n : Nat} (ctx : Ctx n) (rlab rptn : Array Nat) (level : Nat) (st : Search n) : Prop

A saved cheap boundary and its implicit automorphism pair.

• positive : 0 < st.noncheaplevel
• labSize : st.lab.size = n
• ptnSize : st.ptn.size = n
• rootEnd : st.ptn[st.ptn.size - 1]! ≤ 1
• pair : st.noncheaplevel < level → PairOk ctx.g rptn rlab 1 (fmptn st.lab st.ptn st.noncheaplevel n).fst (fmptn st.lab st.ptn st.noncheaplevel n).snd

theorem Hex.GraphIso.Nauty.CheapOk.ready {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {level : Nat} {st : Search n} (h : CheapOk ctx rlab rptn level st) (hbound : st.noncheaplevel ≤ level) (hne : level ≠ st.noncheaplevel) : PairOk ctx.g rptn rlab 1 (fmptn st.lab st.ptn st.noncheaplevel n).fst (fmptn st.lab st.ptn st.noncheaplevel n).snd

The saved boundary supplies a valid pair when its guard permits pruning.

theorem Hex.GraphIso.Nauty.CheapOk.ofFrames {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {level : Nat} {st out : Search n} (h : CheapOk ctx rlab rptn level st) (hlab : out.lab = st.lab) (hptn : out.ptn = st.ptn) (hncl : out.noncheaplevel = st.noncheaplevel) : CheapOk ctx rlab rptn level out

The cheap-boundary invariant depends only on the current labelling, partition, and boundary level.

theorem Hex.GraphIso.Nauty.recover_fmptn {n : Nat} {st : Search n} {inf level saved : Nat} (hsize : n ≤ st.ptn.size) (hend : st.ptn[st.ptn.size - 1]! ≤ saved) (hsaved : saved ≤ level) (hinf : level < inf) : fmptn (recover inf level st).lab (recover inf level st).ptn saved n = fmptn st.lab st.ptn saved n

Reopening below level preserves every fmptn frozen at or above the root and at or below level.

theorem Hex.GraphIso.Nauty.CheapOk.recover {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {current level inf : Nat} {st : Search n} (h : CheapOk ctx rlab rptn current st) (hle : level ≤ current) (hlevel : 1 ≤ level) (hinf : level < inf) : CheapOk ctx rlab rptn level (Nauty.recover inf level st)

Recovery either parks the boundary just below the next child, where the strict pair condition is dormant, or retains an older frozen pair.

theorem Hex.GraphIso.Nauty.CheapOk.park {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {old current boundary : Nat} {st : Search n} (h : CheapOk ctx rlab rptn old st) (hpos : 0 < boundary) (hcurrent : current ≤ boundary) : CheapOk ctx rlab rptn current { lab := st.lab, ptn := st.ptn, active := st.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 := boundary, 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 }

Writing a boundary at or above the logical level suspends the pair condition without changing the partition facts needed to revive it.

theorem Hex.GraphIso.Nauty.CheapOk.next {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {level : Nat} {st : Search n} (h : CheapOk ctx rlab rptn level st) (hpair : st.noncheaplevel = level → PairOk ctx.g rptn rlab 1 (fmptn st.lab st.ptn st.noncheaplevel n).fst (fmptn st.lab st.ptn st.noncheaplevel n).snd) : CheapOk ctx rlab rptn (level + 1) st

A valid pair at the current boundary extends the invariant through the next logical level.

theorem Hex.GraphIso.Nauty.CheapOk.refine {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {level numcells : Nat} {st out : Search n} (h : CheapOk ctx rlab rptn level st) (hlevel : 1 ≤ level) (hlab : out.lab = (Nauty.refine ctx level st.lab st.ptn st.active numcells).lab) (hptn : out.ptn = (Nauty.refine ctx level st.lab st.ptn st.active numcells).ptn) (hncl : out.noncheaplevel = st.noncheaplevel) : CheapOk ctx rlab rptn level out

Refinement only splits at the current level and permutes within the old current cells, so every pair frozen at a strictly smaller level is unchanged.

theorem Hex.GraphIso.Nauty.CheapOk.breakout {n : Nat} {ctx : Ctx n} {rlab rptn : Array Nat} {level tc len o : Nat} {st out : Search n} (h : CheapOk ctx rlab rptn (level + 1) st) (hlevel : 1 ≤ level) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) (hlab : out.lab = (Nauty.breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst) (hptn : out.ptn = st.ptn.set! tc (level + 1)) (hncl : out.noncheaplevel = st.noncheaplevel) : CheapOk ctx rlab rptn (level + 1) out

Individualizing inside a current cell does not change the implicit pair frozen at an older cheap boundary.

theorem Hex.GraphIso.Nauty.CheapOk.root {n k : Nat} {G : Colored n k} {ctx : Ctx n} {numcells : Nat} {st : Search n} (hn0 : 0 < n) (hok : SearchOk G 1 numcells st) (hncl : st.noncheaplevel = 1) : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) 1 st

The initial search boundary is one, so its strict pair condition is empty at the root.