def Hex.GraphIso.Nauty.Sparse.checkDiff {n : Nat} (a b : Key n) : Bool

Distinguish complete sparse keys using their proved native order.

Equations

• Hex.GraphIso.Nauty.Sparse.checkDiff a b = (a.cmp b != Ordering.eq)

theorem Hex.GraphIso.Nauty.Sparse.checkDiff_sound {n : Nat} {a b : Key n} (h : checkDiff a b = true) : a ≠ b

theorem Hex.GraphIso.Nauty.Sparse.not_isomorphic_of_checkKeys {n k : Nat} {G H : Sparse.Colored n k} {cg ch : CertNode} {bg bh : Key n} (hg : checkKey G cg bg = true) (hh : checkKey H ch bh = true) (hd : checkDiff bg bh = true) : ¬Sparse.Isomorphic G H

Two accepted sparse canonical certificates with differing keys prove non-isomorphism. Certificate failure is never used as a negative verdict.