Certificates and Lean 4 formalisation for two distinct eigenvalues at the sparsity threshold

Résumé fourni par la source

Lean 4 / Mathlib sources and exact rational certificates supporting the note "A counterexample and a threshold theorem for graphs with two distinct eigenvalues". For a graph G, q(G) is the minimum number of distinct eigenvalues over the real symmetric matrices with off-diagonal zero pattern prescribed by G (diagonal free). This deposit formally verifies: (i) q(K_{1,1,3}) = 3, a counterexample to Conjecture 5.5 of Barrett, Fallat, Furst, Nasserasr, Rooney and Tait (Electronic Journal of Linear Algebra 42 (2026) 146-161); (ii) a reduction schema from a tight faithful orthogonal representation to a matrix with two distinct eigenvalues and the Strong Spectral Property, parametric in n and r; (iii) q_M(complement(C_m) join K_2) = 2 for every odd m >= 5, as a single theorem over the family; and (iv) a four-zone partition of the level e(complement(G)) = n-2 with the exceptional graph isolated. Certificates are rational identities, so verification is exact. All Lean theorems compile against Mathlib with no unproved lemmas (no sorry).

Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.