"""Independent exact check of the Lean argument for Graffiti 290 and 292 (no Lean involved).

For each graph of girth >= 5: S = sum of gravity entries (exact rationals),
  check S <= (2m)^2/n, meanGravity <= 1, meanGravityOffDiagonal <= 1,
  max|lambda| <= Delta <= m, -lambda_{n-1} <= m/mean (both readings), lambda_+ <= n/mean.
"""
from fractions import Fraction as F
import itertools, random
import networkx as nx, numpy as np

def check(G, name):
    n, m = G.number_of_nodes(), G.number_of_edges()
    if n < 2 or m == 0: return None
    d = dict(G.degree()); dist = dict(nx.all_pairs_shortest_path_length(G))
    S = F(0)
    for u in G:
        for v in G:
            if u != v and v in dist[u]:
                S += F(d[u]*d[v], (n-1)*dist[u][v])
    mean, moff = S/(n*n), S/(n*(n-1))
    ev = np.sort(np.linalg.eigvalsh(nx.to_numpy_array(G)))[::-1]
    lam_n1 = ev[n-2]; Delta = max(d.values()); eps = 1e-9
    lam_plus = min([x for x in ev if x > eps], default=None)
    res = {
      'S<=(2m)^2/n': S <= F(4*m*m, n), 'mean<=1': mean <= 1, 'moff<=1': moff <= 1,
      '|lam|<=Delta<=m': abs(ev).max() <= Delta+eps and Delta <= m,
      '290 (n^2)': -lam_n1 <= m/float(mean)+eps, '290 (off)': -lam_n1 <= m/float(moff)+eps,
      '292 (n^2)': lam_plus is None or lam_plus <= n/float(mean)+eps,
      '292 (off)': lam_plus is None or lam_plus <= n/float(moff)+eps}
    return res, float(S/F(4*m*m, n))

def girth_ok(G):
    g = nx.girth(G)
    return g == 0 or g >= 5 or g == float('inf')

graphs = [(nx.cycle_graph(5),'C5'),(nx.petersen_graph(),'Petersen'),(nx.heawood_graph(),'Heawood'),
          (nx.hoffman_singleton_graph(),'Hoffman-Singleton'),(nx.cycle_graph(17),'C17'),(nx.path_graph(10),'P10'),
          (nx.star_graph(8),'K_{1,8}'),(nx.complete_graph(2),'K2'),(nx.path_graph(3),'P3'),
          (nx.LCF_graph(20,[10,7,4,-4,-7,10,-4,7,-7,4],2),'Desargues'),(nx.pappus_graph(),'Pappus')]
for n in range(2, 8):                      # every graph in the atlas up to 7 vertices
    pass
atlas = [g for g in nx.graph_atlas_g() if 2 <= g.number_of_nodes() <= 7 and nx.is_connected(g) and girth_ok(g)]
graphs += [(g, f'atlas#{i}') for i, g in enumerate(atlas)]
random.seed(292)
for t in range(300):                       # random girth >= 5 graphs by edge insertion with rejection
    n = random.randint(8, 40); G = nx.empty_graph(n)
    for _ in range(4*n):
        u, v = random.sample(range(n), 2)
        if G.has_edge(u, v): continue
        if nx.has_path(G, u, v) and nx.shortest_path_length(G, u, v) < 4: continue
        G.add_edge(u, v)
    graphs.append((G, f'random{t}'))
fails, worst, count = [], 0.0, 0
for G, name in graphs:
    if not girth_ok(G): fails.append((name,'girth')); continue
    r = check(G, name)
    if r is None: continue
    res, ratio = r; count += 1; worst = max(worst, ratio)
    bad = [k for k, ok in res.items() if not ok]
    if bad: fails.append((name, bad))
print(f'graphs checked: {count} (named 11, connected atlas girth>=5 n<=7: {len(atlas)}, random: 300)')
print(f'failures: {fails if fails else "none"}')
print(f'tightest S / ((2m)^2/n): {worst:.6f}  (must be <= 1)')