def Hex.GraphIso.Nauty.Sparse.specCanon {n k : Nat} (G : Sparse.Colored n k) : Sparse.Colored n k

The declarative sparse canonical form, attained by a leaf of the complete unpruned sparse tree. Production equality is a separate search theorem.

Equations

• Hex.GraphIso.Nauty.Sparse.specCanon G = G.relabel (Hex.GraphIso.Nauty.Sparse.canonSpecLabel G)

theorem Hex.GraphIso.Nauty.Sparse.specCanon_iso {n k : Nat} (G : Sparse.Colored n k) : Sparse.Isomorphic G (specCanon G)

theorem Hex.GraphIso.Nauty.Sparse.specCanon_invariant {n k : Nat} {G H : Sparse.Colored n k} (h : Sparse.Isomorphic G H) : specCanon G = specCanon H

Isomorphic sparse inputs have equal declarative forms, including their ordered colour sequences. Canonical labels themselves need not coincide.

theorem Hex.GraphIso.Nauty.Sparse.iso_iff_specCanon_eq {n k : Nat} (G H : Sparse.Colored n k) : Sparse.Isomorphic G H ↔ specCanon G = specCanon H

Equality of the sparse declarative canonical forms characterizes isomorphism, at every order including the empty graph.