Refinement splits cells, so the search terminates with a leaf in hand

The fuel of the search is n + 1, and canonical falls back on the identity labelling if the search comes back empty-handed. This file rules that out.

The measure is the number of cells, numCells. Individualising a vertex of a non-singleton cell creates a new cell start, and refinement never merges cells — that is Refines, proved by following the cell starts through splitCell, splitCellsFrom, refineStep and refineLoop. So each level of the tree has at least one more cell than its parent (numCells_child), the tree has depth at most n, and the fuel is enough (dfsNode_best). The other thing needed is that the first child of a node is never orbit-pruned, which holds because the orbit mark starts out empty and is only refreshed when an automorphism has been found — which happens only at a leaf.

Refinement only splits cells

def IsoGraph.Canon.Refines (n : ℕ) (q p : Part) : Prop

q refines p: every cell of p is a union of cells of q. Since a cell is determined by its start position (Part.WF.cst_eq_iff), this is the same as saying every cell start of p is still a cell start of q.

Equations

• IsoGraph.Canon.Refines n q p = ∀ i < n, p.cst[i]! = i → q.cst[i]! = i

theorem IsoGraph.Canon.Refines.refl {n : ℕ} (p : Part) : Refines n p p

theorem IsoGraph.Canon.Refines.trans {n : ℕ} {p q r : Part} (h1 : Refines n q r) (h2 : Refines n p q) : Refines n p r

theorem IsoGraph.Canon.splitCell_cst_self {n : ℕ} {cnt : Array ℕ} {c : ℕ} {st : SplitState} (hinv : SplitInv n cnt st) (hc : c < n) (hcst : st.cst[c]! = c) : (splitCell cnt c st).cst[c]! = c

The cell being split keeps its start: the first fragment starts where the cell did.

theorem IsoGraph.Canon.splitCell_refines {n : ℕ} {cnt : Array ℕ} {c : ℕ} {st : SplitState} (hinv : SplitInv n cnt st) (hc : c < n) (hcst : st.cst[c]! = c) : Refines n (splitCell cnt c st).part st.part

Splitting one cell leaves every cell start in place.

theorem IsoGraph.Canon.splitCellsFrom_refines {n : ℕ} {cnt cells : Array ℕ} (hnd : cells.toList.Nodup) (fuel j : ℕ) (st : SplitState) : SplitInv n cnt st → (∀ (j' : ℕ), j ≤ j' → j' < cells.size → cells[j']! < n ∧ st.cst[cells[j']!]! = cells[j']!) → Refines n (splitCellsFrom cnt cells fuel j st).part st.part

theorem IsoGraph.Canon.refineStep_refines {n : ℕ} {f : ℕ → ℕ → Bool} {p : Part} (hp : Part.WF n p) {s : ℕ} (hs : s < n) (hcst : p.cst[s]! = s) (inW : Array Bool) (tr : UInt64) : Refines n (refineStep (Graph.ofOracle n f) p inW s tr (Scratch.empty n)).1 p

theorem IsoGraph.Canon.refineLoop_refines {n : ℕ} {f : ℕ → ℕ → Bool} (fuel : ℕ) (p : Part) (inW : Array Bool) (tr : UInt64) : Part.WF n p → Refines n (refineLoop (Graph.ofOracle n f) fuel p inW tr (Scratch.empty n)).1 p

theorem IsoGraph.Canon.refine_refines {n : ℕ} {f : ℕ → ℕ → Bool} {p : Part} (hp : Part.WF n p) (inW : Array Bool) (tr : UInt64) : Refines n (refine (Graph.ofOracle n f) p inW tr).1 p

Individualisation creates a cell, refinement keeps it

theorem IsoGraph.Canon.cenTargetFrom_big {n : ℕ} {c : Array ℕ} (fuel i j : ℕ) : cenTargetFrom c n fuel i = some j → c[j]! - j > 1

theorem IsoGraph.Canon.targetCell_big {n : ℕ} {p : Part} {c : ℕ} (h : p.targetCell n = some c) : p.cen[c]! - c > 1

The target cell has at least two vertices.

theorem IsoGraph.Canon.individualize_refines {n : ℕ} {p : Part} {v : ℕ} (hp : Part.WF n p) (hv : v < n) : Refines n (individualize p v).1 p

theorem IsoGraph.Canon.individualize_new_start {n : ℕ} {p : Part} {v : ℕ} (hp : Part.WF n p) (hv : v < n) (hbig : p.cst[p.pos[v]!]! + 1 < p.cen[p.pos[v]!]!) : (individualize p v).1.cst[p.cst[p.pos[v]!]! + 1]! = p.cst[p.pos[v]!]! + 1

Individualising v makes c + 1 a cell start, where c is the start of v's cell.

theorem IsoGraph.Canon.child_refines {n : ℕ} {f : ℕ → ℕ → Bool} {p : Part} {v : ℕ} (hp : Part.WF n p) (hv : v < n) : Refines n (child (Graph.ofOracle n f) p v).1 p

The number of cells, and why the search terminates in n levels

def IsoGraph.Canon.numCells (n : ℕ) (p : Part) : ℕ

The number of cells of p inside {0, …, n-1}.

Equations

• IsoGraph.Canon.numCells n p = {i ∈ Finset.range n | p.cst[i]! = i}.card

theorem IsoGraph.Canon.numCells_le {n : ℕ} (p : Part) : numCells n p ≤ n

theorem IsoGraph.Canon.numCells_mono {n : ℕ} {p q : Part} (h : Refines n q p) : numCells n p ≤ numCells n q

theorem IsoGraph.Canon.numCells_lt {n : ℕ} {p q : Part} (h : Refines n q p) {i0 : ℕ} (hi0 : i0 < n) (h1 : q.cst[i0]! = i0) (h2 : p.cst[i0]! ≠ i0) : numCells n p < numCells n q

theorem IsoGraph.Canon.numCells_child {n : ℕ} {f : ℕ → ℕ → Bool} {p : Part} {c v : ℕ} (hp : Part.WF n p) (htc : p.targetCell n = some c) (hv : v < n) (hcell : p.cst[p.pos[v]!]! = c) : numCells n p < numCells n (child (Graph.ofOracle n f) p v).1

Each level of the search splits a cell. This is what bounds the depth of the tree by n and makes the fuel n + 1 enough to reach a leaf.

The search always finishes with a leaf in hand

theorem IsoGraph.Canon.pruneNode_abortTo {invPath : Array UInt64} {st st' : St} (h : pruneNode invPath st = some st') : st'.abortTo = st.abortTo

theorem IsoGraph.Canon.pruneNode_none_best {invPath : Array UInt64} {st : St} (h : pruneNode invPath st = none) : st.best.isSome = true

theorem IsoGraph.Canon.leafUpdate_best_isSome (G : Graph) (path : Array ℕ) (invPath : Array UInt64) (lab : Array ℕ) (st : St) : (leafUpdate G path invPath lab st).best.isSome = true

theorem IsoGraph.Canon.orbRefresh_eq {G : Graph} {path processed : Array ℕ} {orb : Orbits} {st : St} (h : orb.nGens = st.autos.size) : orbRefresh G path processed orb st = orb

theorem IsoGraph.Canon.dfsNode_best (n : ℕ) (f : ℕ → ℕ → Bool) (fuel : ℕ) (path : Array ℕ) (invPath : Array UInt64) (p : Part) (st : St) : Part.WF n p → n + 1 ≤ numCells n p + fuel → (st.abortTo.isSome = true → st.best.isSome = true) → (dfsNode (Graph.ofOracle n f) fuel path invPath p st).best.isSome = true

The search always ends holding a leaf. The fuel n + 1 is enough because every level of the tree splits a cell, so a node at depth d has at least d + 1 cells and the tree has depth at most n - 1; and the first child of a node is never orbit-pruned, so the descent always reaches a leaf, which leafUpdate stores.

theorem IsoGraph.Canon.canonSt_best_isSome (n : ℕ) (f : ℕ → ℕ → Bool) : (canonSt n f).best.isSome = true

The search always returns a genuine leaf: canonical never falls back on the identity labelling.

theorem IsoGraph.Canon.canonical_cert_leaf (n : ℕ) (f : ℕ → ℕ → Bool) : ∃ (b : Leaf), (canonSt n f).best = some b ∧ (canonical (Graph.ofOracle n f)).cert = b.cert ∧ Leafkey n f (leafKey b.invPath b.cert)