Nodes of the search tree

dfsNode carries three arguments that are only meaningful together: the array path of the vertices individualised so far, the invariant path invPath, and the current partition p. Node n f path invPath p is the ghost relation saying that these three really do come from individualising path from the root, in order.

It packages the facts that the recursion needs about a node it is sitting at:

• Node.wf — the partition is well-formed;
• Node.path_lt — the individualised vertices are vertices;
• Node.reach — a leaf below this node is a leaf of the whole tree (so a key found here is a legitimate candidate for the maximum);
• Node.auto_partEquiv — the partition is invariant under any automorphism fixing path pointwise, which is exactly the hypothesis reach_child_auto needs and exactly what usableAutos filters for.

Nodes of the search tree

inductive IsoGraph.Canon.Node (n : ℕ) (f : ℕ → ℕ → Bool) : Array ℕ → Array UInt64 → Part → Prop

Node n f path invPath p says that the search reaches the node (invPath, p) by individualising the vertices of path, in order. It is the ghost information that ties together the three arguments path, invPath and p of dfsNode.

• root {n : ℕ} {f : ℕ → ℕ → Bool} : Node n f #[] (rootInv n f) (rootPart n f)
• step {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {invPath : Array UInt64} {p : Part} {c v : ℕ} (h : Node n f path invPath p) (hc : p.targetCell n = some c) (hv : v < n) (hcell : p.cst[p.pos[v]!]! = c) : Node n f (path.push v) (childInv (Graph.ofOracle n f) invPath p v) (child (Graph.ofOracle n f) p v).1

theorem IsoGraph.Canon.Node.wf {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {invPath : Array UInt64} {p : Part} (h : Node n f path invPath p) : Part.WF n p

theorem IsoGraph.Canon.Node.path_lt {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {invPath : Array UInt64} {p : Part} (h : Node n f path invPath p) (i : ℕ) : i < path.size → path[i]! < n

theorem IsoGraph.Canon.Node.reach {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {invPath : Array UInt64} {p : Part} (h : Node n f path invPath p) {k : List (List UInt64)} (hk : Reach n f invPath p k) : Leafkey n f k

Every leaf below a node of the tree is a leaf of the whole tree.

theorem IsoGraph.Canon.Node.auto_partEquiv {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {invPath : Array UInt64} {p : Part} (h : Node n f path invPath p) {g : Array ℕ} (hg : IsAutoArr n f g) (hfix : ∀ i < path.size, g[path[i]!]! = path[i]!) : PartEquiv n (fun (x : ℕ) => g[x]!) p p

The partition at a node is invariant under any automorphism fixing its path. This is what makes orbit pruning legitimate: usableAutos keeps exactly the automorphisms fixing path.