CAS-assisted proof of Tito Pieza's conjecture re Emma Lehmer's quintic

MO438701.sage

R.<n> = PolynomialRing(QQ)

def p(x):
	return x^5 + n^2*x^4 - (2*n^3 + 6*n^2 + 10*n + 10)*x^3 + (n^4 + 5*n^3 + 11*n^2 + 15*n + 5)*x^2 + (n^3 + 4*n^2 + 10*n + 10)*x + 1

def s(x):
	return (n + 2 + n*x - x*x) / (1 + 2*x + n*x)

R2.<xtmp> = PolynomialRing(FractionField(R))
R3.<x1> = R2.quotient(p(xtmp))

x2 = s(x1)
x3 = s(x2)
x4 = s(x3)
x5 = s(x4)
roots = [x1, x2, x3, x4, x5]

# Validate that they're all distinct
print(len(set(roots)), "distinct roots")

# Validate that they're all roots
print(["ok" if p(x) == 0 else "fail" for x in roots])

# (x2^4 x3^3 x4^2 x5)^{1/5} / (x1^4 x2^3 x3^2 x4)^{1/5} = (x1 x2 x3 x4 x5 / x1^5)^{1/5} = -1 / x1
# So (x1^4 x2^3 x3^2 x4)^{1/5} + (x2^4 x3^3 x4^2 x5)^{1/5} + (x3^4 x4^3 x5^2 x1)^{1/5} + (x4^4 x5^3 x1^2 x2)^{1/5} + (x5^4 x1^3 x2^2 x3)^{1/5}
#  = (x1^4 x2^3 x3^2 x4)^{1/5} (1 - 1/x1 + 1/(x1 x2) - 1/(x1 x2 x3) + 1/(x1 x2 x3 x4))
# and since none of the roots are zero, the fifth root part is non-zero.

print("Theorem proven" if 1 - 1 / x1 + 1 / (x1 * x2) - 1 / (x1 * x2 * x3) + 1 / (x1 * x2 * x3 * x4) == 0 else "Proof failed")