def Hex.GraphIso.Nauty.Max.root {n k : Nat} (G : Colored n k) : Frame n

The actual coloured root, with no preceding refinement codes.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Max.root_input {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : NodeInput G { g := rowsOf G } 100 (n + 2) true (root G) [] [] fun (x : Nat) => none

The root supplies every input of the conditional maximum theorem.

theorem Hex.GraphIso.Nauty.Max.root_key {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : Frame.key { g := rowsOf G } 100 (root G) = canonSpecKey G

The frozen root's subtree is precisely the nonempty specification.

theorem Hex.GraphIso.Nauty.Max.root_best {n k : Nat} (G : Colored n k) (hn0 : 0 < n) (rules : Rules G 100) : SearchState.best { g := rowsOf G } (runState n (rowsOf G) (initialPartition G).fst (initialPartition G).snd).snd = some (canonSpecKey G)

The conditional local rules determine the search's final incumbent. No root invariant or final-state identification is an assumed parameter.

theorem Hex.GraphIso.Nauty.Max.key_eq {n k : Nat} (G : Colored n k) (hn0 : 0 < n) (rules : Rules G 100) : canonSpecKey G = tracedKey G

The local maximum rules imply the public nonempty key equality.

theorem Hex.GraphIso.Nauty.Max.spec_zero {k : Nat} (G : Colored 0 k) : canonSpecKey G = { codes := [], rows := [] }

The empty specification has no refinement code.

theorem Hex.GraphIso.Nauty.Max.traced_zero {k : Nat} (G : Colored 0 k) : tracedKey G = { codes := [codeSentinel], rows := [] }

The empty trace still appends the sentinel, so its certificate uses the separate empty-graph case rather than nonempty key equality.