32.2. The Petersen graph three ways🔗

The Petersen graph is the standard first nontrivial example, and the library's family generators construct it twice: as the generalized Petersen graph Families.gpetersen 5 2, an outer pentagon 0..4, an inner five-point star 5..9 stepping by two, and spokes joining the rings; and as the Kneser graph Families.kneser 5 2, whose vertices are the two-element subsets of a five-element set in colexicographic order, joined when disjoint. The two families are unrelated at general parameters; that G(5, 2) and K(5, 2) are isomorphic is a coincidence special to these values, and proving it is the first example below. One explicit edge list shows the generalized Petersen numbering concretely, checked against the general construction. Neither claim mentions colours, so both are stated on bare Graph 10 values.

open Hex Hex.GraphIso

namespace HexGraphIsoChapterExample

def petersen : Graph 10 := Families.gpetersen 5 2

def kneser52 : Graph 10 := Families.kneser 5 2

-- The generalized Petersen numbering, concretely.
#guard Graph.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)] =
  Families.gpetersen 5 2

-- The two canonical searches compose into an explicit
-- vertex permutation between the presentations, and the
-- decision agrees.
#guard (Graph.findIso petersen kneser52).isSome
#guard Graph.isIso petersen kneser52

-- The tactic closes the positive goal through the
-- kernel-replayed transporter check.
example : Graph.Isomorphic petersen kneser52 := by⊢ petersen.Isomorphic kneser52 graph_isoAll goals completed! 🐙

The pentagonal prism, Families.gpetersen 5 1, is the interesting negative companion: like the Petersen graph it has ten vertices, every one of degree three, so degree refinement alone does not settle the question. The tactic closes it by replaying one canonical-key certificate per side in the kernel: each replay pins that graph's nauty-semantic canonical key, and two different keys refute the isomorphism.

theorem

Hex.GraphIso.Nauty.checkKey_sound {n k : ℕ}
  {G : Hex.GraphIso.Colored n k} {cert : Hex.GraphIso.Nauty.CertNode}
  {B : Hex.GraphIso.Nauty.Key n}
  (h : Hex.GraphIso.Nauty.checkKey G cert B = true) :
  Hex.GraphIso.Nauty.canonSpecKey G = B
Hex.GraphIso.Nauty.checkKey_sound
  {n k : ℕ} {G : Hex.GraphIso.Colored n k}
  {cert : Hex.GraphIso.Nauty.CertNode}
  {B : Hex.GraphIso.Nauty.Key n}
  (h :
    Hex.GraphIso.Nauty.checkKey G cert B =
      true) :
  Hex.GraphIso.Nauty.canonSpecKey G = B

A successful certificate replay pins the nauty-semantic canonical key.

def prism5 : Graph 10 := Families.gpetersen 5 1

example : ¬ Graph.Isomorphic petersen prism5 := by⊢ ¬petersen.Isomorphic prism5 graph_isoAll goals completed! 🐙