Strongly cospectral sets in seven-dimensional cubelike graphs

Two vertices of a graph are strongly cospectral if their orthogonal projections onto each adjacency eigenspace agree up to sign. Árnadóttir and Godsil asked in 2021 whether their upper bound 2d/2-1 for the size of a pairwise strongly cospectral set in a cubelike graph on 2ᵈ vertices, d≥3, is tight in every dimension in its range. We prove that every such set in every cubelike graph on $128$ vertices has size at most four, whereas their bound gives eight. Their connected construction attains four, so the maximum in dimension seven is exactly four and the all-dimensions tightness question has a negative answer. The proof combines character sums, congruences and a second-moment bound with an exact finite inequality certified by linear programming duality. The universal upper bound, including the certificate checks, is formalized in Lean; attainment is checked separately. Checked in Lean from the definitions; not yet reviewed by experts. Produced by AI models under the author's direction.