theorem Hex.GraphIso.Nauty.boundaryPolicy {n : Nat} (ctx : Ctx n) (inf tcLevel bound saved : Nat) : Generic.BoundedPolicy ctx inf tcLevel bound fun (st : Search n) => st.noncheaplevel = saved ∨ bound < st.noncheaplevel

A boundary retained above a call stays fixed until the call creates a deeper boundary.

theorem Hex.GraphIso.Nauty.node_boundary {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells : Nat} {st : Search n} (hlevel : 0 < level) : (node false ctx inf tcLevel fuel level numcells st).snd.noncheaplevel = st.noncheaplevel ∨ level ≤ (node false ctx inf tcLevel fuel level numcells st).snd.noncheaplevel

An off-path call can only replace its entry boundary below its receiving ancestor.

@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Boundary {n k : Nat} (G : Colored n k) (ctx : Ctx n) (level : Nat) (st : Search n) : Prop

The saved implicit pair is meaningful only strictly below its admission boundary.

Equations

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

theorem Hex.GraphIso.Nauty.Boundary.congr {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level : Nat} {st out : Search n} (h : Boundary G ctx level st) (hl : out.lab = st.lab) (hp : out.ptn = st.ptn) (hn : out.noncheaplevel = st.noncheaplevel) : Boundary G ctx level out

Bookkeeping preserves the frozen pair when its defining fields agree.

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

Refinement preserves every pair frozen strictly above the current node.

theorem Hex.GraphIso.Nauty.initial_boundary {n k : Nat} (G : Colored n k) (hn0 : 0 < n) (ctx : Ctx n) : Boundary G ctx 1 (initial n (initialPartition G).fst (initialPartition G).snd)

The initial state has no active frozen pair.

theorem Hex.GraphIso.Nauty.Boundary.of_out {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level : Nat} {st out : Search n} (h : Boundary G ctx level st) (hlevel : 1 < level) (hout : SearchOut G (level - 1) level st out) (hpos : 0 < out.noncheaplevel) (hn : out.noncheaplevel = st.noncheaplevel ∨ level ≤ out.noncheaplevel) : Boundary G ctx level out

A call's partition receipt transports every still-active frozen pair.

theorem Hex.GraphIso.Nauty.Boundary.node {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells : Nat} {st : Search n} (h : Boundary G ctx level st) (hn0 : 0 < n) (hlevel : 1 < level) (hok : SearchOk G level numcells st) : Boundary G ctx level (Nauty.node false ctx (n + 2) tcLevel fuel level numcells st).snd

An off-path child returns with the implicit pair at every surviving older boundary.

theorem Hex.GraphIso.Nauty.Boundary.recover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {current level : Nat} {st : Search n} (h : Boundary G ctx current st) (hle : level ≤ current) (hlevel : 1 ≤ level) (hinf : level < n + 2) : Boundary G ctx level (Nauty.recover (n + 2) level st)

Recovery revives an older boundary or parks a new one below the next child.

theorem Hex.GraphIso.Nauty.compare_noncheap {n : Nat} (level code : Nat) (st : Search n) : (compareCodes level code st).noncheaplevel = st.noncheaplevel

Comparing codes preserves the boundary level.

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

Choosing either target preserves the boundary level.

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

Classification preserves the boundary level.

theorem Hex.GraphIso.Nauty.cheap_bound {n level : Nat} {st : Search n} (first : Bool) (h : st.noncheaplevel ≤ level) : (cheapCheck first level st).noncheaplevel ≤ level + 1

The guard's boundary is at most the next child's level.

theorem Hex.GraphIso.Nauty.recover_bound {n : Nat} (level : Nat) (st : Search n) : (recover (n + 2) level st).noncheaplevel ≤ level + 1

Recovery parks a deeper boundary at the next child's level.

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

Comparing codes leaves the saved pair unchanged.

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

Target selection leaves the saved pair unchanged.

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

Classification fills scratch data without changing the saved pair.

theorem Hex.GraphIso.Nauty.Boundary.leaf {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level : Nat} {st : Search n} (h : Boundary G ctx level st) (leaf : Leaf) : Boundary G ctx level (leafExit leaf level st).snd

Leaf actions retain the saved pair, including after an admission.

theorem Hex.GraphIso.Nauty.Boundary.cheap {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level : Nat} {st : Search n} (h : Boundary G ctx level st) (first : Bool) (hlevel : 1 ≤ level) (hpair : cheapautom st.ptn level n = true → PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (fmptn st.lab st.ptn level n).fst (fmptn st.lab st.ptn level n).snd) : Boundary G ctx (level + 1) (cheapCheck first level st)

A successful guard validates a new boundary; a failed guard parks it below the next child.

theorem Hex.GraphIso.Nauty.Boundary.child {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level tc tv : Nat} {st : Search n} {cell : VSet n} (h : Boundary G ctx (level + 1) st) (first : Bool) (hlevel : 1 ≤ level) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (htv : cell.mem tv = true) : Boundary G ctx (level + 1) (Nauty.child first level tc tv st)

Individualizing within the current cell preserves the frozen ancestor pair.

theorem Hex.GraphIso.Nauty.refined_pair {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) (heq : Equitable ctx level (SearchState.refined ctx level numcells st).lab (SearchState.refined ctx level numcells st).ptn) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hcheap : cheapautom (SearchState.refined ctx level numcells st).ptn level n = true) : have R := SearchState.refined ctx level numcells st; PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (fmptn R.lab R.ptn level n).fst (fmptn R.lab R.ptn level n).snd

A refined equitable node passing the cheap guard supplies the root ledger pair.

theorem Hex.GraphIso.Nauty.Boundary.recover_child {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level : Nat} {st : Search n} (h : Boundary G ctx (level + 1) st) (hlevel : 1 ≤ level) (hinf : level < n + 2) : Boundary G ctx (level + 1) (Nauty.recover (n + 2) level st)

Returning to a parent preserves its boundary pair for the next child, including equality.