"""Independent check of Graffiti 295 on graphs of girth >= 5 (no Lean involved).

n_+(D) = number of positive eigenvalues of the distance matrix (numeric, symmetric eigensolver).
Mean gravity (both readings) uses exact rationals. Checks n_+(D) <= n/mean for both readings,
and records n_+(D) for named graphs.
"""
from fractions import Fraction as F
import random
import networkx as nx, numpy as np

def gravity_sum(G):
    n = G.number_of_nodes(); d = dict(G.degree()); dist = dict(nx.all_pairs_shortest_path_length(G))
    return sum((F(d[u]*d[v], (n-1)*dist[u][v]) for u in G for v in G if u != v and v in dist[u]), F(0))

def n_plus(G):
    nodes = list(G); idx = {v: i for i, v in enumerate(nodes)}
    dist = dict(nx.all_pairs_shortest_path_length(G))
    D = np.zeros((len(nodes), len(nodes)))
    for u in nodes:
        for v, k in dist[u].items():
            D[idx[u], idx[v]] = k
    return int((np.linalg.eigvalsh(D) > 1e-9).sum())

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

named = [(nx.cycle_graph(5),'C5'),(nx.petersen_graph(),'Petersen'),(nx.heawood_graph(),'Heawood'),
         (nx.hoffman_singleton_graph(),'Hoffman-Singleton'),(nx.LCF_graph(24,[12,7,-7],8),'McGee'),
         (nx.LCF_graph(30,[-13,-9,7,-7,9,13],5),'Tutte-Coxeter'),(nx.pappus_graph(),'Pappus'),
         (nx.LCF_graph(20,[10,7,4,-4,-7,10,-4,7,-7,4],2),'Desargues'),(nx.dodecahedral_graph(),'Dodecahedral'),
         (nx.path_graph(10),'P10'),(nx.star_graph(8),'K_{1,8}'),(nx.complete_graph(2),'K2')]
atlas = [(g, f'atlas#{i}') for i, g in enumerate(nx.graph_atlas_g()) if 2 <= g.number_of_nodes() <= 7 and nx.is_connected(g) and girth_ok(g)]
random.seed(295); rnd = []
for t in range(300):
    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) or (nx.has_path(G, u, v) and nx.shortest_path_length(G, u, v) < 4): continue
        G.add_edge(u, v)
    rnd.append((G.subgraph(max(nx.connected_components(G), key=len)).copy(), f'random{t}'))
fails, rows, count = [], [], 0
for G, name in named + atlas + rnd:
    n = G.number_of_nodes()
    if n < 2 or not girth_ok(G) or not nx.is_connected(G): continue
    S = gravity_sum(G); mean, moff = S/(n*n), S/(n*(n-1)); k = n_plus(G); count += 1
    ok = mean <= 1 and moff <= 1 and k <= n/mean and k <= n/moff
    if not ok: fails.append(name)
    if (G, name) in named: rows.append(f'  {name:18s} n={n:3d} n_+(D)={k:3d}  n/mean={float(n/mean):9.3f}  n/mean_off={float(n/moff):9.3f}')
print(f'connected girth>=5 graphs checked: {count} (named {len(named)}, atlas n<=7 {len(atlas)}, random 300)')
print('failures:', fails if fails else 'none')
print('named graphs:'); print('\n'.join(rows))