theorem Hex.GraphIso.Sparse.canon_eq_specCanon {n k : Nat} (G : Colored n k) : canon G = Nauty.Sparse.specCanon G

The total native sparse canonical form is the declarative maximum's form, at every order. The empty graph is unique; the nonempty case reads the literal production label from the proved exact maximum.

theorem Hex.GraphIso.Sparse.canon_invariant {n k : Nat} {G H : Colored n k} (h : Isomorphic G H) : canon G = canon H

Isomorphic native sparse inputs have identical canonical forms, including the ordered colour sequence.

theorem Hex.GraphIso.Sparse.iso_iff_canon_eq {n k : Nat} (G H : Colored n k) : Isomorphic G H ↔ canon G = canon H

theorem Hex.GraphIso.Sparse.canon_relabel {n k : Nat} (G : Colored n k) (l : Label n) : canon (G.relabel l) = canon G

theorem Hex.GraphIso.Sparse.canon_idempotent {n k : Nat} (G : Colored n k) : canon (canon G) = canon G

theorem Hex.GraphIso.Sparse.findIso_complete {n k : Nat} {G H : Colored n k} (h : Isomorphic G H) : ∃ (p : Perm n), findIso G H = some p

The actual total sparse decision returns a transporter for every isomorphic pair; no logical search limit remains in this API.

theorem Hex.GraphIso.Sparse.isIso_eq_true_iff {n k : Nat} (G H : Colored n k) : isIso G H = true ↔ Isomorphic G H

theorem Hex.GraphIso.Sparse.findIso_isSome_iff {n k : Nat} (G H : Colored n k) : (findIso G H).isSome = true ↔ Isomorphic G H

theorem Hex.GraphIso.Sparse.isomorphic_of_isIso {n k : Nat} {G H : Colored n k} (h : isIso G H = true) : Isomorphic G H

theorem Hex.GraphIso.Sparse.isIso_eq_false_iff {n k : Nat} (G H : Colored n k) : isIso G H = false ↔ ¬Isomorphic G H

theorem Hex.GraphIso.Sparse.findIso_eq_none_iff {n k : Nat} (G H : Colored n k) : findIso G H = none ↔ ¬Isomorphic G H