English
For a strongly regular graph with parameters (n,k,ℓ,μ) and any semiring α, the adjacency matrix A satisfies A^2 = k I + ℓ A + μ C, where C is the adjacency matrix of the complement Gᶜ.
Русский
Для сильного регулярного графа с параметрами (n,k,ℓ,μ) и произвольного полупринятого полупрямого, матрица смежности A удовлетворяет A^2 = k I + ℓ A + μ C, где C — матрица смежности комплемента Gᶜ.
LaTeX
$$$A^2 = k\,I + \ell\,A + \mu\,C$, где $A = G.adjMatrix\!_\alpha$ и $C = G^{\mathsf{c}}.adjMatrix\!_\alpha$.$$
Lean4
/-- Let `A` and `C` be the adjacency matrices of a strongly regular graph with parameters `n k ℓ μ`
and its complement respectively and `I` be the identity matrix,
then `A ^ 2 = k • I + ℓ • A + μ • C`. `C` is equivalent to the expression `J - I - A`
more often found in the literature, where `J` is the all-ones matrix. -/
theorem matrix_eq {α : Type*} [Semiring α] (h : G.IsSRGWith n k ℓ μ) :
G.adjMatrix α ^ 2 = k • (1 : Matrix V V α) + ℓ • G.adjMatrix α + μ • Gᶜ.adjMatrix α :=
by
ext v w
simp only [adjMatrix_pow_apply_eq_card_walk, Set.coe_setOf, Matrix.add_apply, Matrix.smul_apply, adjMatrix_apply,
compl_adj]
rw [Fintype.card_congr (G.walkLengthTwoEquivCommonNeighbors v w)]
obtain rfl | hn := eq_or_ne v w
· rw [← Set.toFinset_card]
simp [commonNeighbors, ← neighborFinset_def, h.regular v]
· simp only [Matrix.one_apply_ne' hn.symm, ne_eq, hn]
by_cases ha : G.Adj v w <;>
simp only [ha, ite_true, ite_false, add_zero, zero_add, nsmul_eq_mul, smul_zero, mul_one, not_true_eq_false,
not_false_eq_true, and_false, and_self]
· rw [h.of_adj v w ha]
· rw [h.of_not_adj hn ha]
