32.6. Performance🔗

The Lean implementation runs the same algorithm as nauty in the strictest sense: conformance testing pins the visited-node counters, so both programs traverse exactly the same search tree on every conformance case. Every timing difference is therefore a per-node constant factor of the implementation, never an algorithmic difference, and the one way that factor could grow with the vertex count would be a loop over vertices where nauty runs a word operation. The search keeps its vertex sets packed sixty-three to a word, so a least-squares fit of per-node cost against n on the benchmark corpus gives hex the same exponent as nauty on every family: n^1.7 to n^1.9 on grids, Paley graphs, circulants and random graphs, n^1.3 on Kneser graphs and n^1.0 on Johnson graphs, in each case within 0.2 of nauty's, and the hex/nauty ratio is 7.7 below 64 vertices and 7.1 above. CI refits every recorded sweep and fails when a family's hex exponent exceeds nauty's by more than 0.2. The table shows the factor on four parametrised families: grids, where refinement discretizes quickly; Paley graphs, refinement's hard case among the sparse families; and the dense Latin-square and Kneser graphs. The hex column is canonicalize, which carries the theorems of this chapter as it stands: no certificate is produced or replayed on that path.

Measured on chungus2, 2026-09-05, minimum over repeated runs; regenerate with scripts/bench/graphiso_cactus_sweep.sh. On ten-vertex pairs like the examples of this chapter, the kernel-checked graph_iso proof costs roughly 20 milliseconds on a positive goal and 0.7 to 0.9 seconds on a negative one. That price is separate from the table and does not shrink with it: a kernel proof still replays a certificate inside the kernel, whereas canonicalize runs no replay at all. For breadth across the whole benchmark corpus, see the cactus plots in reports/figures/ in the repository: hexgraphiso-canon-cactus.svg for canonical labelling over the deterministic families, and hexgraphiso-pairs-cactus.svg for the proof obligations. The latter plots the negative pairs only. For the reason just given the two polarities differ by well over an order of magnitude, so a single curve over both would describe neither; the figure's caption carries the positive median for comparison.