The search meets its specification

The two halves of the correctness proof meet here.

• dfsNode_reach (soundness, IsoGraph/Canon/Search.lean) says the leaf the search settles on really is a leaf of the whole tree.
• dfsNode_dom (optimality, IsoGraph/Canon/Optimal.lean) says every leaf of the whole tree is dominated by it.

Instantiating the second at the root gives canonSt_dom, and together they give canonSt_bestKey — the search's answer satisfies BestKey, the specification stated back in IsoGraph/Canon/Search.lean. Since BestKey is manifestly an isomorphism invariant (bestKey_transfer) and determines its key uniquely (bestKey_unique), the certificate the search returns does not depend on how the vertices were named: canonical_cert_relabel.

That is exactly what Spec.LabellingInvariant needs, once certOf_get is used to read the adjacency matrix back out of the packed certificate (canonical_get).

theorem IsoGraph.Canon.stopDepth_zero (ab : Option ℕ) : stopDepth 0 ab = 0

theorem IsoGraph.Canon.ancReach_root (n : ℕ) (f : ℕ → ℕ → Bool) (k : List (List UInt64)) : ancReach n f #[] 0 k ↔ Leafkey n f k

theorem IsoGraph.Canon.canonSt_dom (n : ℕ) (f : ℕ → ℕ → Bool) (k : List (List UInt64)) (hk : Leafkey n f k) : Dom (canonSt n f) k

The search finds the best leaf. Instantiating dfsNode_dom at the root: the state the search ends in dominates every leaf of the whole tree.

theorem IsoGraph.Canon.canonSt_bestKey (n : ℕ) (f : ℕ → ℕ → Bool) (b : Leaf) (hb : (canonSt n f).best = some b) : BestKey n f (leafKey b.invPath b.cert)

The search meets its specification. The key of the leaf it settles on is the largest key of any leaf of the (unpruned) tree.

theorem IsoGraph.Canon.canonical_get (n : ℕ) (f : ℕ → ℕ → Bool) {i j : ℕ} (hi : i < n) (hj : j < n) : certGet n (canonical (Graph.ofOracle n f)).cert i j = f (canonical (Graph.ofOracle n f)).lab[i]! (canonical (Graph.ofOracle n f)).lab[j]!

Reading the winner's certificate back gives the adjacency in the canonical order.

theorem IsoGraph.Canon.canonical_cert_relabel (n : ℕ) (f : ℕ → ℕ → Bool) {s : ℕ → ℕ} (hs : IsPerm n s) : (canonical (Graph.ofOracle n fun (v w : ℕ) => f (s v) (s w))).cert = (canonical (Graph.ofOracle n f)).cert

The winner's certificate is an isomorphism invariant. The search on the renamed graph settles on a leaf with the same certificate as the search on the original.