@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Sparse.CheapBoundary {n k : Nat} (G : Sparse.Colored n k) (level : Nat) (st : State n) : Prop

The implicit pair at every strictly older cheap boundary is valid at the original ordered-colour partition. The logical level determines when the saved pair is available to pruning.

Equations

• Hex.GraphIso.Nauty.Sparse.CheapBoundary G level st = Hex.GraphIso.Nauty.Boundary G.toDense (Hex.GraphIso.Nauty.Sparse.Graph.context G.graph) level st.frame

theorem Hex.GraphIso.Nauty.Sparse.Ready.pair {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hc : cheapautom st.ptn level n = true) : PairOk (Graph.context G.graph).g (initPtn n (n + 2) (Nauty.initialPartition G.toDense).snd) (Nauty.initialPartition G.toDense).fst 1 (fmptn st.lab st.ptn level n).fst (fmptn st.lab st.ptn level n).snd

An equitable native partition passing the cheap guard supplies the implicit root pair used by the actual pruning workspace.

theorem Hex.GraphIso.Nauty.Sparse.CheapBoundary.congr {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st out : State n} (h : CheapBoundary G level st) (hl : out.lab = st.lab) (hp : out.ptn = st.ptn) (he : out.noncheaplevel = st.noncheaplevel) : CheapBoundary G level out

theorem Hex.GraphIso.Nauty.Sparse.CheapBoundary.visit {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : CheapBoundary G level st) (hn : 0 < n) (hl : 1 ≤ level) (hi : NodeInv G level numcells st) : CheapBoundary G level (Sparse.visit (Graph.ofGraph G.graph) level numcells st).snd.snd

Native refinement preserves every strictly older saved pair by its proved caller-frame effect; the root's strict pair condition is empty.

theorem Hex.GraphIso.Nauty.Sparse.CheapBoundary.record {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : CheapBoundary G level st) (code : Nat) : CheapBoundary G level (recordFirst level code st)

theorem Hex.GraphIso.Nauty.Sparse.CheapBoundary.compare {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : CheapBoundary G level st) (code : Nat) : CheapBoundary G level (compareCodes level code st)

theorem Hex.GraphIso.Nauty.Sparse.CheapBoundary.target {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : CheapBoundary G level st) (first : Bool) (tcLevel numcells : Nat) : CheapBoundary G level (chooseTarget first (Graph.ofGraph G.graph) tcLevel level numcells st).snd.snd.snd

theorem Hex.GraphIso.Nauty.Sparse.CheapBoundary.classify {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : CheapBoundary G level st) (numcells : Nat) : CheapBoundary G level (Sparse.classify (Graph.ofGraph G.graph) level numcells st).snd

theorem Hex.GraphIso.Nauty.Sparse.CheapBoundary.leaf {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : CheapBoundary G level st) (leaf : Leaf) : CheapBoundary G level (leafExit leaf level st).snd

theorem Hex.GraphIso.Nauty.Sparse.CheapBoundary.cheap {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : CheapBoundary G level st) (hn : 0 < n) (hl : 1 ≤ level) (hr : Ready G level numcells st) (first : Bool) : CheapBoundary G (level + 1) (cheapCheck first level st)

A passing native guard establishes the implicit pair, while a failing guard parks the pair condition at the next child's depth.

theorem Hex.GraphIso.Nauty.Sparse.CheapBoundary.child {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : CheapBoundary G (level + 1) st) (hl : 1 ≤ level) (first : Bool) {tc tv : Nat} {cell : VSet n} (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) : CheapBoundary G (level + 1) (Generic.Policy.child first level tc tv st)

Native individualization and cache invalidation preserve every pair frozen above the child.

theorem Hex.GraphIso.Nauty.Sparse.CheapBoundary.node {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : CheapBoundary G level st) (hn : 0 < n) (hl : 1 < level) (hi : NodeInv G level numcells st) (tcLevel fuel : Nat) : CheapBoundary G level (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd

Every completed off-path call preserves still-active saved pairs; only a new boundary at or below that call may replace the old boundary.

theorem Hex.GraphIso.Nauty.Sparse.CheapBoundary.recover_child {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : CheapBoundary G (level + 1) st) (hl : 1 ≤ level) (hi : level < n + 2) : CheapBoundary G (level + 1) (Generic.Policy.recover (n + 2) level st)

Recovery revives an older pair, including equality at the next child's logical level, using the literal native cache-invalidating operation.

theorem Hex.GraphIso.Nauty.Sparse.initial_boundary {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; CheapBoundary G 1 (initial (Graph.ofGraph G.graph) p.fst p.snd)

Initialization starts at boundary one with no active implicit pair.