#!/usr/bin/env python3
"""Symbolic verification of the proposed Graffiti 292 proof chain."""
import sympy as sp

x = sp.symbols('x', positive=True)

# For n >= 7 it remains to prove, with t = sqrt(4n-3) >= 5:
# 4(n-1)n/(1+t)^2 >= sqrt(n(1+t)/2).
# Substitute n=(t^2+3)/4, square positive sides, and clear denominators.
t = sp.symbols('t', real=True)
n = (t**2 + 3) / 4
left = 4 * (n - 1) * n / (1 + t) ** 2
right_squared = n * (1 + t) / 2
cleared = sp.factor((left**2 - right_squared) * 32 * (t + 1) ** 4 / (t**2 + 3))
print('cleared_factorization=', cleared)
print('expanded=', sp.expand(cleared))
print('at_t_5=', sp.factor(cleared.subs(t, 5)))
derivative = sp.factor(sp.diff(cleared, t))
print('derivative=', derivative)

# Verify monotonic positivity of the cleared polynomial on t>=5 by shifting t=u+5.
u = sp.symbols('u', nonnegative=True)
shifted = sp.Poly(sp.expand(cleared.subs(t, u + 5)), u)
print('shifted_coefficients=', shifted.all_coeffs())
assert all(coefficient > 0 for coefficient in shifted.all_coeffs())
assert sp.factor(cleared) == 2 * (t + 1)**2 * (t**4 - 4*t**3 - 2*t**2 - 12*t + 1)
print('OK: cleared polynomial has strictly positive coefficients after t=u+5.')