"""EXACT verification: Hoffman-Singleton refutes Graffiti 284.

Statement (WotW, girth >= 5): min dual degree <= - lambda_min(Distance matrix),
where dual degree of v = mean degree of the neighbors of v.

Strategy: NO floating point in the decisive chain.
  1. Build HS, verify n=50, m=175, 7-regular, girth 5, connected (integer checks).
  2. Verify the SRG identity A^2 + A - 6I = J exactly over the integers.
     On the orthogonal complement of the all-ones vector this forces every
     adjacency eigenvalue mu to satisfy mu^2 + mu - 6 = 0, i.e. mu in {2, -3};
     the all-ones vector has eigenvalue 7 (regularity).
  3. Verify by exact BFS that every off-diagonal distance is 1 or 2, so
     D = 2(J - I) - A exactly (integer matrix identity).
  4. Therefore the D-eigenvalues are: 2(n-1) - 7 = 91 on the all-ones vector,
     and -2 - mu in {-4, 1} on its complement. lambda_min(D) = -4 EXACTLY.
  5. min dual degree = 7 (7-regular). Conjecture asserts 7 <= 4. FALSE. Margin 3.
"""
import numpy as np
import networkx as nx

G = nx.hoffman_singleton_graph()
n = G.number_of_nodes()
m = G.number_of_edges()
assert n == 50 and m == 175, (n, m)
assert nx.is_connected(G)
degs = [d for _, d in G.degree()]
assert set(degs) == {7}, "not 7-regular"
assert nx.girth(G) == 5, nx.girth(G)
print("HS: n=50 m=175 7-regular girth=5 connected  [OK]")

nodes = sorted(G.nodes())
A = nx.to_numpy_array(G, nodelist=nodes, dtype=np.int64)   # exact 0/1 integers
assert (A == A.T).all() and (np.diag(A) == 0).all()

# 2) SRG identity over the integers
J = np.ones((n, n), dtype=np.int64)
I = np.eye(n, dtype=np.int64)
lhs = A @ A + A - 6 * I
assert (lhs == J).all(), "SRG identity A^2 + A - 6I = J FAILED"
print("A^2 + A - 6I == J exactly (integer arithmetic)  [OK]")
print(" => adjacency spectrum is {7^1, 2^a, (-3)^b}; trace: 7+2a-3b=0, a+b=49 -> a=28, b=21")
# multiplicity check via traces (exact integers):
tr_A = int(np.trace(A)); tr_A2 = int(np.trace(A @ A))
assert tr_A == 0 and tr_A2 == 2 * m == 350
# 7^2 + 4a + 9b = 350 with a+b=49 -> 4a + 9b = 301 -> solve: a=28, b=21
a_, b_ = 28, 21
assert 49 + 4*a_ + 9*b_ == 350 - 0*49 or True
assert 7 + 2*a_ - 3*b_ == 0 and a_ + b_ == 49 and 49 + 4*a_ + 9*b_ == 350
print("multiplicities: 7^1, 2^28, (-3)^21 (trace-certified)  [OK]")

# 3) distance matrix exactly via BFS
D = np.zeros((n, n), dtype=np.int64)
for i, u in enumerate(nodes):
    lengths = nx.single_source_shortest_path_length(G, u)
    for j, v in enumerate(nodes):
        D[i, j] = lengths[v]
off = D[~np.eye(n, dtype=bool)]
assert set(off.tolist()) == {1, 2}, "diameter != 2"
assert (D == 2*(J - I) - A).all(), "D != 2(J-I) - A"
print("D == 2(J-I) - A exactly; diameter 2  [OK]")
print(" => D-spectrum: 2(n-1)-7 = 91 on all-ones; -2-mu on 1-perp: mu=2 -> -4, mu=-3 -> 1")
print(" => lambda_min(D) = -4 EXACTLY (multiplicity 28)")

# float sanity cross-check only (not part of the proof)
eigD = np.linalg.eigvalsh(D.astype(float))
print(f"float cross-check: min eig D = {eigD.min():.12f} (expect -4)")

# 4) the conjecture
min_dual = 7  # every neighbor of every vertex has degree 7
rhs = 4       # -lambda_min(D)
print()
print(f"Graffiti 284 asserts: min_dual({min_dual}) <= -lambda_min(D) ({rhs})")
print(f"7 <= 4 is FALSE. counterexample margin = {min_dual - rhs} (exact integer)")
print()
print("GRAFFITI 284 REFUTED by the Hoffman-Singleton graph. VERIFIED EXACTLY.")