def Hex.GraphIso.Nauty.labColor {n k : Nat} (G : Colored n k) (lab : Array Nat) (i : Nat) : Nat

The colour value at position i of a labelling.

Equations

• Hex.GraphIso.Nauty.labColor G lab i = if h : i < lab.size ∧ lab[i]! < n then ↑G.coloring.cells[⟨lab[i]!, ⋯⟩] else 0

def Hex.GraphIso.Nauty.labelColorSorted {n k : Nat} (G : Colored n k) (lab : Array Nat) : Bool

Positions list colours in nondecreasing order.

Equations

• Hex.GraphIso.Nauty.labelColorSorted G lab = (List.range n).all fun (i : Nat) => decide (i + 1 = n) || decide (Hex.GraphIso.Nauty.labColor G lab i ≤ Hex.GraphIso.Nauty.labColor G lab (i + 1))

def Hex.GraphIso.Nauty.checkCanon {n k : Nat} (G : Colored n k) (cert : CertNode) (B : Key n) (lab : Array Nat) : Option (CanonResult n k)

Validate a certificate together with the claimed canonical labelling: the replay must accept the key, and the labelling's leaf rows must be the key's rows. Returns the canonical form and label.

Equations

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

theorem Hex.GraphIso.Nauty.checkCanon_sound {n k : Nat} {G : Colored n k} {cert : CertNode} {B : Key n} {lab : Array Nat} {res : CanonResult n k} (h : checkCanon G cert B lab = some res) : canonSpecKey G = B ∧ res.form = G.relabel res.label ∧ Isomorphic G res.form ∧ B.rows = leafRows { g := rowsOf G } lab

A successful checkCanon identifies the claimed key with the spec key, exhibits the form as a relabelling, and shows the form isomorphic to the input.

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

Produce a checked CanonResult: run the untrusted key search and validate its candidate together with the transcribed search's canonical labelling in ONE trusted checkCanon replay (which contains the checkKey certificate replay: validating through certifyKey? first would replay the certificate twice). The transcription supplies nauty's exact label tie-breaking. Every ingredient stays untrusted until the single replay accepts.

Equations

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

theorem Hex.GraphIso.Nauty.searchResult?_eq_of_checkCanon {n k : Nat} {G : Colored n k} {cert : CertNode} {B : Key n} {res : CanonResult n k} (h : checkCanon G cert B (runColored G).canonlab = some res) : searchResult? G = some res

A successful checkCanon on the transcribed search's own labelling forces the transcription to succeed with the same result: both build the CanonResult from (runColored G).canonlab by the same checked construction.

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

Whenever the single trusted replay accepts (certifyCanon? succeeds), the fast transcription agrees with it exactly.

def Hex.GraphIso.Nauty.checkDiff {n : Nat} (B1 B2 : Key n) : Bool

Executable disequality of two canonical keys: the lexicographic comparison finds the first differing entry.

Equations

• Hex.GraphIso.Nauty.checkDiff B1 B2 = (Hex.GraphIso.Nauty.keyCmp B1 B2 != Ordering.eq)

theorem Hex.GraphIso.Nauty.checkDiff_sound {n : Nat} {B1 B2 : Key n} (h : checkDiff B1 B2 = true) : B1 ≠ B2

theorem Hex.GraphIso.Nauty.not_isomorphic_of_key_ne {n k : Nat} {G H : Colored n k} {BG BH : Key n} (hG : canonSpecKey G = BG) (hH : canonSpecKey H = BH) (hne : BG ≠ BH) : ¬Isomorphic G H

Distinct spec keys separate isomorphism classes.

theorem Hex.GraphIso.Nauty.not_isomorphic_of_certs {n k : Nat} {G H : Colored n k} {certG certH : CertNode} {BG BH : Key n} {labG labH : Array Nat} {resG resH : CanonResult n k} (hG : checkCanon G certG BG labG = some resG) (hH : checkCanon H certH BH labH = some resH) (hd : checkDiff BG BH = true) : ¬Isomorphic G H

Two checked certificates with differing keys prove non-isomorphism.

theorem Hex.GraphIso.Nauty.not_isomorphic_of_checkKeys {n k : Nat} {G H : Colored n k} {certG certH : CertNode} {BG BH : Key n} (hG : checkKey G certG BG = true) (hH : checkKey H certH BH = true) (hd : checkDiff BG BH = true) : ¬Isomorphic G H

Two replayed key certificates with differing keys prove non-isomorphism: the Boolean form of not_isomorphic_of_certs. The kernel computes two checkKey replays and one key comparison, with no achieving labelling required.

theorem Hex.GraphIso.Nauty.invPerm_go_size (lab : Array Nat) (l : List Nat) (inv : Array Nat) : (invPerm.go lab l inv).size = inv.size

theorem Hex.GraphIso.Nauty.invPerm_go_untouched (lab : Array Nat) (l : List Nat) (inv : Array Nat) (w : Nat) : (∀ (j : Nat), j ∈ l → lab[j]! ≠ w) → (invPerm.go lab l inv)[w]! = inv[w]!

theorem Hex.GraphIso.Nauty.invPerm_go_get (lab : Array Nat) (l : List Nat) (inv : Array Nat) (i : Nat) : i ∈ l → (∀ (j : Nat), j ∈ l → lab[j]! = lab[i]! → j = i) → lab[i]! < inv.size → (invPerm.go lab l inv)[lab[i]!]! = i

theorem Hex.GraphIso.Nauty.invPerm_size (lab : Array Nat) : (invPerm lab).size = lab.size

theorem Hex.GraphIso.Nauty.getElem!_invPerm (lab : Array Nat) (hinj : ∀ (a b : Nat), a < lab.size → b < lab.size → lab[a]! = lab[b]! → a = b) {i : Nat} (hi : i < lab.size) (hv : lab[i]! < lab.size) : (invPerm lab)[lab[i]!]! = i

theorem Hex.GraphIso.Nauty.getElem!_invPerm_lt {lab : Array Nat} (hn0 : 0 < lab.size) (v : Nat) : (invPerm lab)[v]! < lab.size

theorem Hex.GraphIso.Nauty.rowOf_relabel {n k : Nat} {G : Colored n k} {l : Label n} {lab : Array Nat} (hsz : lab.size = n) (hl : ∀ (i : Nat) (h : i < n), ↑(l.get ⟨i, h⟩) = lab[i]!) {i : Nat} (hi : i < n) : rowOf (G.relabel l) i = (rowsOf G)[lab[i]!]!.permset (invPerm lab)

theorem Hex.GraphIso.Nauty.rowsOf_relabel_eq_leafRows {n k : Nat} {G : Colored n k} {l : Label n} {lab : Array Nat} (hsz : lab.size = n) (hl : ∀ (i : Nat) (h : i < n), ↑(l.get ⟨i, h⟩) = lab[i]!) : rowsOf (G.relabel l) = (leafRows { g := rowsOf G } lab).toArray

The claimed labelling's leaf rows are exactly the rows of the relabelled graph.

theorem Hex.GraphIso.Nauty.checkCanon_inv {n k : Nat} {G : Colored n k} {cert : CertNode} {B : Key n} {lab : Array Nat} {res : CanonResult n k} (h : checkCanon G cert B lab = some res) : lab.size = n ∧ res.form = G.relabel res.label ∧ (∀ (i : Nat) (hi : i < n), ↑(res.label.get ⟨i, hi⟩) = lab[i]!) ∧ checkKey G cert B = true ∧ B.rows = leafRows { g := rowsOf G } lab ∧ labelColorSorted G lab = true

Everything a successful checkCanon establishes, with the label's entries equal to those of the claimed array.

theorem Hex.GraphIso.Nauty.checkCanon_rows {n k : Nat} {G : Colored n k} {cert : CertNode} {B : Key n} {lab : Array Nat} {res : CanonResult n k} (h : checkCanon G cert B lab = some res) : rowsOf res.form = B.rows.toArray

The rows of a checked canonical form are the key's rows.

theorem Hex.GraphIso.Nauty.checkCanon_sorted {n k : Nat} {G : Colored n k} {cert : CertNode} {B : Key n} {lab : Array Nat} {res : CanonResult n k} (h : checkCanon G cert B lab = some res) (i : Nat) (hi1 : i + 1 < n) : ↑res.form.coloring.cells[i] ≤ ↑res.form.coloring.cells[i + 1]

The colours of a checked canonical form are nondecreasing along the vertex order.

theorem Hex.GraphIso.Nauty.pairwise_le_of_adjacent {f : Nat → Nat} {m : Nat} (h : ∀ (i : Nat), i + 1 < m → f i ≤ f (i + 1)) : List.Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) (List.map f (List.range m))

def Hex.GraphIso.Nauty.colorList {n k : Nat} (K : Colored n k) : List Nat

The colour value at each vertex, as a plain list.

Equations

• Hex.GraphIso.Nauty.colorList K = List.map (Hex.GraphIso.Nauty.keyOf K) (List.range n)

theorem Hex.GraphIso.Nauty.count_colorList {n k : Nat} (K : Colored n k) {c : Nat} (hc : c < k) : List.count c (colorList K) = (colorClass K c).length

theorem Hex.GraphIso.Nauty.count_colorList_ge {n k : Nat} (K : Colored n k) {c : Nat} (hc : k ≤ c) : List.count c (colorList K) = 0

theorem Hex.GraphIso.Nauty.colorList_perm_of_lengths {n k : Nat} {G' H' G H : Colored n k} (hG : Isomorphic G G') (hH : Isomorphic H H') (hGH : ∀ (c : Nat), c < k → (colorClass G c).length = (colorClass H c).length) : (colorList G').Perm (colorList H')

theorem Hex.GraphIso.Nauty.checkCanon_form_eq {n k : Nat} {G H : Colored n k} {certG certH : CertNode} {B : Key n} {labG labH : Array Nat} {resG resH : CanonResult n k} (hG : checkCanon G certG B labG = some resG) (hH : checkCanon H certH B labH = some resH) (hlen : ∀ (c : Nat), c < k → (colorClass G c).length = (colorClass H c).length) : resG.form = resH.form

Two checked canonical forms with the same key and the same colour class sizes are equal.

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

Executable equality of colour class sizes.

Equations

• Hex.GraphIso.Nauty.cellSizesCheck G H = (List.range k).all fun (c : Nat) => (Hex.GraphIso.Nauty.colorClass G c).length == (Hex.GraphIso.Nauty.colorClass H c).length

theorem Hex.GraphIso.Nauty.cellSizesCheck_sound {n k : Nat} {G H : Colored n k} (h : cellSizesCheck G H = true) (c : Nat) : c < k → (colorClass G c).length = (colorClass H c).length

theorem Hex.GraphIso.Nauty.isomorphic_of_certs {n k : Nat} {G H : Colored n k} {certG certH : CertNode} {B : Key n} {labG labH : Array Nat} {resG resH : CanonResult n k} (hG : checkCanon G certG B labG = some resG) (hH : checkCanon H certH B labH = some resH) (hcs : cellSizesCheck G H = true) : Isomorphic G H

Two checked certificates with the same key and matching colour class sizes prove isomorphism.