Prove2Me

Row-profile census for diagonal-00 rows of an orbit-matrix candidate

Proved
Conway99.diag_zero_offdiag_profile

by WillR · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsconway-99orbit-matrixstrongly-regular-graphs

Let CC be a 9×99\times 9 matrix over N\mathbb{N} satisfying the Conway99 orbit-matrix equations: CC is symmetric, every row sums to 1414, and (C2)ij+cij(C^2)_{ij} + c_{ij} equals 3434 on the diagonal and 2222 off the diagonal. For a row ii with diagonal entry cii=0c_{ii} = 0, the eight off-diagonal entries sum to 1414 with square-sum 3434. Their value multiset is then exactly one of {0,0,2,2,2,2,3,3}\{0,0,2,2,2,2,3,3\}, {0,1,1,1,2,3,3,3}\{0,1,1,1,2,3,3,3\}, {0,1,1,2,2,2,2,4}\{0,1,1,2,2,2,2,4\}, or {1,1,1,1,1,2,3,4}\{1,1,1,1,1,2,3,4\}, stated as fiber counts over the value classes 00 through 55 (larger entries are excluded by the square sum). This is the diagonal-00 case of the row-profile census feeding the trace-1010 branch of Wilbrink's Theorem 5.

Preamble
import Mathlib.Data.Matrix.Basic
import Mathlib.Algebra.BigOperators.Fin
Formal statement
open scoped BigOperators

namespace Conway99

theorem diag_zero_offdiag_profile
    (C : Matrix (Fin 9) (Fin 9) ℕ) (hsymm : ∀ i j, C i j = C j i)
    (hrow : ∀ i, ∑ j, C i j = 14)
    (hsq : ∀ i j, (∑ k, C i k * C k j) + C i j = (if i = j then 12 else 0) + 22)
    (i : Fin 9) (hi : C i i = 0) :
    ((((Finset.univ.erase i).filter (fun k => C i k = 0)).card = 2 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 1)).card = 0 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 2)).card = 4 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 3)).card = 2 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 4)).card = 0 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 5)).card = 0) ∨
     (((Finset.univ.erase i).filter (fun k => C i k = 0)).card = 1 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 1)).card = 3 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 2)).card = 1 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 3)).card = 3 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 4)).card = 0 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 5)).card = 0) ∨
     (((Finset.univ.erase i).filter (fun k => C i k = 0)).card = 1 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 1)).card = 2 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 2)).card = 4 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 3)).card = 0 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 4)).card = 1 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 5)).card = 0) ∨
     (((Finset.univ.erase i).filter (fun k => C i k = 0)).card = 0 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 1)).card = 5 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 2)).card = 1 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 3)).card = 1 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 4)).card = 1 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 5)).card = 0)) := by sorry

end Conway99
Source
H. A. Wilbrink, 'On the (99,14,1,2) strongly regular graph', EUT Report 84-WSK-03, 1984, Theorem 5, pp. 350-354, https://pure.tue.nl/ws/files/2449333/256699.pdf ; row-moment census for the trace-10, no-four branch.

View graph