theorem Hex.GraphIso.Nauty.keyEq_of_firstRun {n k : Nat} {G : Colored n k} (hn0 : n ≠ 0) {fs : List Nat} {best : Option (Key n)} {eventTrail : FrameTrail} (hroot : FirstRun G { g := rowsOf G } 100 n (n + 2) 1 [] fs (rootSt n (initialPartition G).fst (initialPartition G).snd) (rootOut n (rowsOf G) (initialPartition G).fst (initialPartition G).snd) (initialPartition G).snd.length best FrameTrail.empty eventTrail (firstPathNode { g := rowsOf G } (n + 2) 100 (n + 2) 1 (initialPartition G).snd.length (rootSt n (initialPartition G).fst (initialPartition G).snd)).fst) : canonSpecKey G = tracedKey G

The first-path root result proves equality between the unpruned specification key and the key installed by the transcription, whatever event trail the run reports.

theorem Hex.GraphIso.Nauty.keyEq_of_firstTotal {n k : Nat} (G : Colored n k) (hn0 : 0 < n) (h : FirstTotal G { g := rowsOf G } (n + 2) 100 (n + 2)) : canonSpecKey G = tracedKey G

First-path totality at the root fuel yields the key equality.

theorem Hex.GraphIso.Nauty.certifyCanon?_isSome_zero {k : Nat} (G : Colored 0 k) : (certifyCanon? G).isSome = true

The empty graph is certified without any search.

theorem Hex.GraphIso.Nauty.totalAll {n k : Nat} (G : Colored n k) (ctx : Ctx n) (inf tcLevel runFuel : Nat) : OtherTotal G ctx inf tcLevel runFuel ∧ FirstTotal G ctx inf tcLevel runFuel

Every node of both kinds is total at every executable fuel.

theorem Hex.GraphIso.Nauty.canonSpecKey_eq_tracedKey {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : canonSpecKey G = tracedKey G

The unpruned specification key is the key the transcription installs.

theorem Hex.GraphIso.Nauty.certifyCanon?_isSome {n k : Nat} (G : Colored n k) : (certifyCanon? G).isSome = true

The certified canonicalization always succeeds.

def Hex.GraphIso.Nauty.certifyCanon {n k : Nat} (G : Colored n k) : CanonResult n k

Certificate-checked canonicalization: the transcribed search's answer, accepted through the single trusted checkCanon replay, which always succeeds.

Equations

• Hex.GraphIso.Nauty.certifyCanon G = (Hex.GraphIso.Nauty.certifyCanon? G).get ⋯

theorem Hex.GraphIso.Nauty.certifyCanon?_eq {n k : Nat} (G : Colored n k) : certifyCanon? G = some (certifyCanon G)

theorem Hex.GraphIso.Nauty.certifyCanon_form {n k : Nat} (G : Colored n k) : (certifyCanon G).form = specCanon G

theorem Hex.GraphIso.Nauty.certifyCanon_relabel {n k : Nat} (G : Colored n k) : G.relabel (certifyCanon G).label = (certifyCanon G).form

theorem Hex.GraphIso.Nauty.searchResult?_eq {n k : Nat} (G : Colored n k) : searchResult? G = some (certifyCanon G)

The transcription agrees with the certificate-checked answer on every input.

theorem Hex.GraphIso.Nauty.searchResult?_isSome {n k : Nat} (G : Colored n k) : (searchResult? G).isSome = true

The transcription always answers.