The number of 5-inner equivalence classes of simple graphs on at most five vertices

Abstract

Eilers, Restorff, Ruiz and Sørensen close their geometric classification of graph C^*-algebras with an atlas of small graphs. A simple graph there is a finite directed graph with loops allowed and no multiple edges, and two such graphs with at most M vertices are M-inner equivalent when a chain of five elementary steps — isomorphism, a legal row addition, a legal column addition, deletion of a regular source, a legal collapse — joins them without ever leaving the simple graphs on at most M vertices. Their table records 2,8,35,218 classes for M=1,2,3,4 and a question mark at M=5, the accompanying sentence being that at M=5 they "have not attempted a complete analysis". We prove that the entry is 2172. The proof is a component certificate for the move graph on the 295 128 isomorphism classes of simple graphs with at most five vertices: a spanning forest bounds the number of classes above by 2172, a move-invariant colouring bounds it below by the same number, and the colouring is a complete invariant, so no transversal is shorter and no family of pairwise inequivalent graphs is longer. The same machinery, run at M ≤ 4, returns the published 2,8,35,218 exactly, which is the evidence that the five clauses and their legality conditions have been transcribed correctly; and the two legality conditions that an implementation is most likely to drop — the path condition on the two additions, and the requirement that a collapsed vertex support no loop — are each shown to be load-bearing by an explicit pair of graphs that dropping it would wrongly merge. The theorems below are machine-checked in Lean 4, with no sorry and with the compiled evaluator as the only trusted computational step; the few statements that lie outside the formal development are labelled where they occur. Two structural by-products, computed outside the formal development and labelled as such, are that each of the two vertex-deleting moves is individually redundant at every M ≤ 5 while the two together are not, and that every class contains a graph on exactly M vertices.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 1 · current (opens in a new tab)

   Source snapshot 2026-09-07 03:53 UTC

   File fingerprint

   b260d21310d6d7b35f698fa8381ea36c136cd3ebce082024b31bff393340c6f4