def Hex.GraphIso.rootCodeA (n : Nat) (g : Array (Nauty.VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : Nat

The root refinement code over the packed-set state of the specification.

Equations

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

def Hex.GraphIso.Kernel.rootCode {n k : Nat} (G : Colored n k) (rows : Nat) : Nat

The specification key's head code of a coloured graph whose adjacency rows are packed as the one number rows: a single refinement of the initial partition.

Equations

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

theorem Hex.GraphIso.Kernel.rootCode_eq {n k : Nat} (G : Colored n k) (hn : 2 ≤ n) : (Nauty.canonSpecKey G).codes.head? = some (rootCode G (packRows n G.graph.adjMatrix.data.toList))

Above one vertex the root code is the head of the specification key.

def Hex.GraphIso.Kernel.rootSeparates {n k : Nat} (G H : Colored n k) : Bool

The compiled-side root-code test: whether the root route separates this pair. Evaluated at elaboration time over the Array rows, so the route decision costs one refinement per graph and no kernel work.

Equations

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

def Hex.GraphIso.Kernel.rootDiff {n k : Nat} (G H : Colored n k) (NA NB : Nat) : Bool

The root codes of two coloured graphs disagree: the cheapest kernel check of the negative route, one refinement per graph.

Equations

• Hex.GraphIso.Kernel.rootDiff G H NA NB = (decide (2 ≤ n) && !(Hex.GraphIso.Kernel.rootCode G NA).beq (Hex.GraphIso.Kernel.rootCode H NB))

theorem Hex.GraphIso.Kernel.not_isomorphic_of_rootCode {n k : Nat} {G H : Colored n k} {NA NB : Nat} (hA : packRows n G.graph.adjMatrix.data.toList = NA) (hB : packRows n H.graph.adjMatrix.data.toList = NB) (h : rootDiff G H NA NB = true) : ¬Isomorphic G H

Equalities identifying each graph's packed rows, plus a root-code disagreement, prove non-isomorphism.