36.5. Sparse graphs🔗

A graph given by a short edge list need not allocate an adjacency matrix. SparseGraph n stores n + 1 offsets and a flat array containing the neighbours of every vertex, using O(n + |E|) storage. Each row is sorted, duplicate-free and loopless, and each undirected edge occurs in both directions.

SparseGraph.ofEdges accepts pairs of vertices in Fin n, removes duplicate edges and drops loops. For external data with natural-number endpoints, use SparseGraph.ofEdges?: it rejects loops and out-of-range endpoints instead. Both constructors normalize edge orientation and row order. General input requires sorting, so the storage bound is not a claim that every construction takes linear time.

36.5.1. Canonicalization and isomorphism🔗

Here is the Petersen graph built directly from its fifteen edges. Relabelling swaps vertices 0 and 9; the pentagonal prism replaces the inner star by a pentagon. All three values remain sparse throughout construction and search.

namespace HexGraphIsoSparseExample

def petersen : SparseGraph 10 := SparseGraph.ofEdges
  [(0, 1), (1, 2), (2, 3), (3, 4), (0, 4),
   (5, 7), (7, 9), (6, 9), (6, 8), (5, 8),
   (0, 5), (1, 6), (2, 7), (3, 8), (4, 9)]

def swapEnds : Perm 10 :=
  ⟨#v[9, 1, 2, 3, 4, 5, 6, 7, 8, 0], by⊢ #v[9, 1, 2, 3, 4, 5, 6, 7, 8, 0].toList.Nodup decideAll goals completed! 🐙, by⊢ ∀ (i : Fin 10), i ∈ #v[9, 1, 2, 3, 4, 5, 6, 7, 8, 0].toList decideAll goals completed! 🐙⟩

def renamed : SparseGraph 10 := petersen.relabel swapEnds

def prism : SparseGraph 10 := SparseGraph.ofEdges
  [(0, 1), (1, 2), (2, 3), (3, 4), (0, 4),
   (5, 6), (6, 7), (7, 8), (8, 9), (5, 9),
   (0, 5), (1, 6), (2, 7), (3, 8), (4, 9)]

#guard SparseGraph.ofEdges? 3 [(0, 1), (1, 0)] =
  some (SparseGraph.ofEdges [(0, 1)])
#guard (SparseGraph.ofEdges? 3 [(0, 3)]).isNone
#guard (SparseGraph.ofEdges? 3 [(1, 1)]).isNone

#guard petersen ≠ renamed
#guard SparseGraph.canon petersen =
  SparseGraph.canon renamed
#guard (SparseGraph.findIso petersen renamed).isSome
#guard !(SparseGraph.isIso petersen prism)

example : SparseGraph.Isomorphic petersen renamed := by⊢ petersen.Isomorphic renamed
  graph_isoAll goals completed! 🐙

example : ¬ SparseGraph.Isomorphic petersen prism := by⊢ ¬petersen.Isomorphic prism
  graph_isoAll goals completed! 🐙

SparseGraph.canonicalize returns the form and its label together. A label maps each new vertex to its old vertex. In contrast, the permutation returned by SparseGraph.findIso maps vertices of the first input to vertices of the second. These operations are total, including on the empty graph. A result of none from isomorphism search means that the graphs are not isomorphic, by SparseGraph.findIso_eq_none_iff.

example (G : SparseGraph 10) :
    G.relabel (SparseGraph.label G).perm =
      SparseGraph.canon G :=
  SparseGraph.relabel_label G

example (G H : SparseGraph 10) :
    SparseGraph.Isomorphic G H ↔
      SparseGraph.canon G = SparseGraph.canon H :=
  SparseGraph.iso_iff_canon_eq G H

example : SparseGraph.Isomorphic
    (SparseGraph.empty 0) (SparseGraph.empty 0) := by⊢ (SparseGraph.empty 0).Isomorphic (SparseGraph.empty 0)
  graph_isoAll goals completed! 🐙

36.5.2. Ordered colours and automorphisms🔗

Sparse coloured graphs use the same Coloring as dense graphs. Marking a Petersen edge or a non-edge imposes exactly the constraints from the ordered-colour example.

def edgeMarkA : Sparse.Colored 10 2 :=
  ⟨petersen, HexGraphIsoChapterExample.markPair 0 1⟩
def edgeMarkB : Sparse.Colored 10 2 :=
  ⟨petersen, HexGraphIsoChapterExample.markPair 2 3⟩
def nonedgeMark : Sparse.Colored 10 2 :=
  ⟨petersen, HexGraphIsoChapterExample.markPair 0 2⟩

example : Sparse.Isomorphic edgeMarkA edgeMarkB := by⊢ Sparse.Isomorphic edgeMarkA edgeMarkB
  graph_isoAll goals completed! 🐙

example : ¬ Sparse.Isomorphic edgeMarkA nonedgeMark := by⊢ ¬Sparse.Isomorphic edgeMarkA nonedgeMark
  graph_isoAll goals completed! 🐙

#guard (SparseGraph.autos petersen).order = 120
#guard (SparseGraph.autos petersen).numOrbits = 1
#guard (Sparse.autos edgeMarkA).order = 8

example (p : Perm 10)
    (h : p ∈ (SparseGraph.autos petersen).gens) :
    SparseGraph.IsIso petersen petersen p :=
  SparseGraph.autos_isIso h

end HexGraphIsoSparseExample

Sparse.autos and SparseGraph.autos return generators, orbit representatives, the orbit count and an exact natural-number group order from one traversal. The generators generate every automorphism, by Sparse.autos_complete. Equality of two orbit entries is equivalent to the existence of an automorphism carrying one vertex to the other, by Sparse.autos_sameOrbit. The order is the product of the stabilizer indices accumulated during the search. Its cardinality theorem and the corresponding Mathlib operations appear in the sparse Mathlib section.

36.5.3. Choosing and converting representations🔗

Native sparse input avoids storing or scanning an adjacency matrix. For an existing dense graph, Graph.toSparse scans its n² entries. SparseGraph.toDense allocates a dense matrix. Both conversions preserve adjacency and isomorphism. To compare graphs stored differently, convert one so that both use the same engine. The performance comparison shows how the choice affects different graph families.

Canonicalization itself need not commute with conversion. For two disjoint edges, dense and sparse nauty choose different canonical adjacency matrices:

namespace HexGraphIsoRepresentationExample

def matching : SparseGraph 4 :=
  SparseGraph.ofEdges [(0, 3), (1, 2)]

#guard (Graph.label matching.toDense).toArray =
  #[0, 3, 1, 2]
#guard (SparseGraph.label matching).toArray = #[0, 1, 2, 3]
#guard (SparseGraph.canon matching).toDense ≠
  Graph.canon matching.toDense

end HexGraphIsoRepresentationExample

Each result is a canonical form for its own algorithm. When storing canonical forms as persistent keys, record which engine and options produced them. Traces defines another algorithm and is included in the performance comparison, but has no Lean implementation in this library.

36.5.4. Certificates and tactic limits🔗

graph_iso operates on closed graph expressions and selects the dense or sparse checker from their types. A positive proof checks a literal vertex permutation. For a negative proof, a differing root refinement code suffices when available. Otherwise the tactic produces compact certificates for both sparse canonical keys and replays their literal checkers in the kernel. The sparse checker recomputes sparse refinement and comparisons. The direct canonicalization API does not perform this replay.

The tactic accepts two optional limits. maxSearchNodes bounds search node visits, and maxCertRecords bounds certificate records. Both default to 100000. Exceeding a limit makes the tactic fail; it does not establish non-isomorphism. They can be raised independently:

example : ¬ SparseGraph.Isomorphic
    HexGraphIsoSparseExample.petersen
    HexGraphIsoSparseExample.prism := by⊢ ¬HexGraphIsoSparseExample.petersen.Isomorphic HexGraphIsoSparseExample.prism
  graph_iso (maxSearchNodes := 200000)
    (maxCertRecords := 200000)All goals completed! 🐙

These limits do not apply to the total canonicalization and isomorphism functions. Kernel replay has no estimated-cost cutoff or operation meter. Lean's ordinary heartbeat and recursion-depth options still apply to elaboration.