#!/usr/bin/env python3
"""Exact verification of the stronger, uniform two-path bound for Graffiti 292 (section 2.5).

Claim (girth >= 5, connected, n >= 2):
    lambda_+(G) <= n-1 < n <= n / mean(Gr),   strict, uniform, no case split.

Chain, all exact:
  (S1) sum_v C(d(v),2) <= C(n,2) - m      [no triangle => cherry endpoints non-adjacent;
                                           no C4 => a non-edge has <=1 common neighbour;
                                           so cherries inject into non-edges]
  (S2) sum_v C(d(v),2) = 1/2 sum d^2 - m >= 2m^2/n - m      [Cauchy-Schwarz]
  (S3) => 4 m^2 <= n^2 (n-1)
  (S4) Lemma 1: n/mean(Gr) >= (n-1)n^3/(4m^2) >= (n-1)n^3/(n^2(n-1)) = n   [so mean(Gr) <= 1]
  (S5) lambda_+ <= rho(A) <= Delta <= n-1 < n <= n/mean(Gr)

The counting inequality (S1) and its consequence (S3) are the classical
Kovari-Sos-Turan / Reiman cherry-count; the observation that (S3) composes with
Lemma 1 to settle Graffiti 292 directly and strictly is due to Spanky McDoob
(@59thProfile, private communication, July 2026).

No code shared with the other verifiers. Exact rational arithmetic throughout;
floating point is used only for the eigenvalue upper check lambda_+ <= n-1, which
is a slack inequality (Delta - lambda_+ >= 1) that no rounding can flip.
"""
from fractions import Fraction
from math import comb
import io

import networkx as nx
import numpy as np
import sympy as sp

buf = io.StringIO()
def out(*a):
    s = " ".join(str(x) for x in a)
    print(s); buf.write(s + "\n")

# ---------------------------------------------------------------- symbolic core
n, m = sp.symbols("n m", positive=True)
gap = sp.simplify((n*(n-1)/2 - m) - (2*m**2/n - m))          # non-edges minus CS lower
out("SYMBOLIC")
out("  (C(n,2)-m) - (2m^2/n - m) =", sp.simplify(gap),
    "  ->  >=0  <=>  n^2(n-1) - 4m^2 >= 0")
out("  Lemma 1 at 4m^2 = n^2(n-1):  (n-1)n^3/(n^2(n-1)) =",
    sp.simplify((n-1)*n**3/(n**2*(n-1))), " (= n, so mean(Gr) <= 1)")

# ---------------------------------------------------------------- helpers
def girth(G):
    from collections import deque
    best = float("inf")
    for s in G.nodes():
        dist = {s: 0}; par = {s: None}; dq = deque([s])
        while dq:
            x = dq.popleft()
            for y in G.neighbors(x):
                if y not in dist:
                    dist[y] = dist[x] + 1; par[y] = x; dq.append(y)
                elif par[x] != y:
                    best = min(best, dist[x] + dist[y] + 1)
    return best

def mean_gravity(G):
    N = G.number_of_nodes(); deg = dict(G.degree())
    D = dict(nx.all_pairs_shortest_path_length(G))
    S = Fraction(0)
    for u in G.nodes():
        for v in G.nodes():
            if u != v and v in D[u] and D[u][v] > 0:
                S += Fraction(deg[u] * deg[v], D[u][v])
    return S / Fraction(N - 1) / Fraction(N * N)     # 1/(n-1) factor; mean over all n^2 entries

def check(G):
    N = G.number_of_nodes(); mm = G.number_of_edges()
    deg = [d for _, d in G.degree()]
    cherries = sum(comb(d, 2) for d in deg)
    s1 = cherries <= comb(N, 2) - mm
    s3 = 4 * mm * mm <= N * N * (N - 1)
    mg = mean_gravity(G)
    s4 = mg <= 1
    lam = min(x for x in np.linalg.eigvalsh(nx.to_numpy_array(G)) if x > 1e-9)
    s5 = lam <= N - 1 + 1e-9
    strict = lam < float(Fraction(N, 1) / mg) - 1e-9
    return s1 and s3 and s4 and s5 and strict

# ---------------------------------------------------------------- exhaustive atlas n<=7
total = 0; fails = 0
for G in nx.graph_atlas_g():
    if G.number_of_nodes() < 2 or not nx.is_connected(G):
        continue
    if girth(G) < 5:
        continue
    total += 1
    if not check(G):
        fails += 1
out("ATLAS  (all nontrivial connected girth>=5 graphs, 2<=n<=7)")
out(f"  graphs = {total}   S1&S3&S4&S5&strict failures = {fails}")
assert total == 34 and fails == 0

# ---------------------------------------------------------------- named cages, exact
out("NAMED CAGES  (exact mean gravity as a fraction; strict bound)")
cages = [("Petersen", nx.petersen_graph()), ("Heawood", nx.heawood_graph()),
         ("Pappus", nx.pappus_graph()), ("Desargues", nx.desargues_graph()),
         ("Mobius-Kantor", nx.moebius_kantor_graph())]
for name, G in cages:
    N = G.number_of_nodes(); Delta = max(d for _, d in G.degree())
    mg = mean_gravity(G); rhs = Fraction(N, 1) / mg
    ok = (mg <= 1) and (Delta <= N - 1)
    out(f"  {name:<14} n={N:<3} Delta={Delta:<2} mean(Gr)={str(mg):<9} <=1:{mg<=1}"
        f"  n/mean(Gr)={rhs}  lam_+<=n-1<n<=RHS: {ok}")

out("ALL TWO-PATH CHECKS PASS: lambda_+ <= n-1 < n <= n/mean(Gr), uniformly for n>=2.")

with open(__file__.replace("verify_twopath_292.py", "verify_twopath_292_output.txt"),
          "w", encoding="utf-8") as f:
    f.write(buf.getvalue())