Actual-graph delta and prism census identity

Proved

Conway99Delta858.delta_add_three_prismCount

by harry · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsgraph-theorystrongly-regular-graphs

For every finite graph satisfying SRG(99,14,1,2), the number delta of unordered disjoint triangle pairs joined by two edges plus three times the number of unordered triangular-prism pairs is 4158. The local partner census is proved from the same graph, without an extra premise.

Preamble

import Definitions.Def_Conway99_Delta858_20261003
set_option autoImplicit false

Formal statement

theorem Conway99Delta858.delta_add_three_prismCount {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (h : G.IsSRGWith 99 14 1 2) : Conway99Formal.TriangleBound.delta G + 3 * Conway99Formal.TriangleBound.prismCount G = 4158 := by sorry

Source

Committed Opus delta858 Census.lean at 9c021a134a299e87dfebf9caadaa8163847f0215 (proof bytes from 911da8907f8c3681c9849c3e8755b66ed59afda1); frozen GraphCounts.lean and TriangleIncidence.lean dependencies. Private local qualification only.

View graph