"""Symbolic verification of the terminal inequality for the Graffiti 290 proof.

Chain (girth >= 5, connected, n >= 5):
  RHS = m / mean_Gr >= m * n^2 (n-1) / (4 m^2) = n^2 (n-1) / (4m)      [Lemma 1, d>=1]
  LHS = -lambda_{n-1}(A) <= max|lambda| <= sqrt(2m)                     [trace bound]
  suffices:  n^2 (n-1) / (4m) >= sqrt(2m)  <=>  n^4 (n-1)^2 >= 32 m^3
  with Reiman (C4-free):  m <= B(n) = (n/4)(1 + sqrt(4n-3))
  suffices:  2 n (n-1)^2 >= (1 + sqrt(4n-3))^3
Substituting t = sqrt(4n-3), n = (t^2+3)/4 and clearing:
  (1+t)^2 * Q(t) >= 0  with  Q(t) = t^4 - 2t^3 + 4t^2 - 38t - 29
Claim: Q(u+5) has all positive coefficients => holds for t >= 5, i.e. n >= 7.
n = 5, 6 checked exactly. (m >= n case is even easier: RHS >= n/mean_Gr >= sqrt(2m).)
"""
import sympy as sp

n, m, t, u = sp.symbols('n m t u', positive=True)

# Step A: the reduction  2n(n-1)^2 - (1+t)^3 with n=(t^2+3)/4, times 32, factors:
expr = 32 * (2 * ((t**2+3)/4) * (((t**2+3)/4) - 1)**2 - (1 + t)**3)
expr = sp.expand(expr)
factored = sp.factor(expr)
print("32*(2n(n-1)^2 - (1+t)^3) =", factored)
Q = sp.expand(sp.cancel(expr / (1 + t)**2))
print("Q(t) =", Q)
assert Q == t**4 - 2*t**3 + 4*t**2 - 38*t - 29, Q

# Step B: shift positivity
Qs = sp.expand(Q.subs(t, u + 5))
print("Q(u+5) =", Qs)
coeffs = sp.Poly(Qs, u).all_coeffs()
print("coefficients:", coeffs)
assert all(c > 0 for c in coeffs), "shift positivity FAILED"
print("all coefficients positive => Q(t) > 0 for all t >= 5  (n >= 7)  [OK]")

# Step C: endpoints n = 5, 6 exactly.
for nn in (5, 6):
    tt = sp.sqrt(4*nn - 3)
    val = sp.simplify(2*nn*(nn-1)**2 - (1 + tt)**3)
    print(f"n={nn}: 2n(n-1)^2 - (1+sqrt(4n-3))^3 = {val} = {sp.nsimplify(val)} ~ {float(val):.4f}")
    assert val > 0
print("n=5,6 endpoints positive exactly  [OK]")

# Step D: the m >= n shortcut is implied by the PROVEN 292 terminal:
#   n/mean_Gr >= sqrt(2m) for n >= 7 (already certified in the 292 package);
#   m/mean_Gr = (m/n) * (n/mean_Gr) >= n/mean_Gr when m >= n.
print()
print("TERMINAL INEQUALITY FOR GRAFFITI 290 CERTIFIED SYMBOLICALLY.")