Diagonal census for the trace- no-four orbit-matrix case
ProvedConway99.ten_of_no_four_diag_countcombinatoricsconway-99orbit-matrixstrongly-regular-graphs
Let be a matrix over whose diagonal entries lie in , whose diagonal sums to , and with no diagonal entry equal to . Then exactly five diagonal entries equal and four equal . Indeed every diagonal entry is or , so with entries equal to the trace condition gives and the nine diagonal positions give . This pins the row-type multiset used by the profile census in 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 ten_of_no_four_diag_count
(C : Matrix (Fin 9) (Fin 9) ℕ)
(hdiag : ∀ i, C i i = 0 ∨ C i i = 2 ∨ C i i = 4)
(htr : ∑ i, C i i = 10)
(hfour : ∀ i, C i i ≠ 4) :
(Finset.univ.filter (fun i => C i i = 2)).card = 5 ∧
(Finset.univ.filter (fun i => C i i = 0)).card = 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 ; diagonal census for the trace-10, no-four branch.