Every entry is at most in the no-four orbit-matrix case
ProvedConway99.no_four_all_entries_le_fourcombinatoricsconway-99orbit-matrixstrongly-regular-graphs
Let be a matrix over satisfying the Conway99 orbit-matrix equations (symmetric, row sums , equal to on the diagonal and off it), with every diagonal entry in and no diagonal entry equal to . Then every entry of is at most . Indeed each row has diagonal or , and the row-profile census gives fiber counts with no s in every case, while a direct square-sum argument excludes entries above . This makes the entry domains finite and explicit for the trace-, no-four 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 no_four_all_entries_le_four
(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)
(hdiag : ∀ i, C i i = 0 ∨ C i i = 2 ∨ C i i = 4)
(hfour : ∀ i, C i i ≠ 4) :
∀ i j, C i j ≤ 4 := 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 ; entry bound for the trace-10, no-four branch.