Integral roots of the quintic resolvent sextic

The quintic resolvent sextic is monic over ℤ, so each of its rational roots is integral. This identifies the rational root condition used in the Galois-theoretic resolvent criterion with the integral root evidence carried by TauCeti.HasSexticRoot.

Main results

• TauCeti.exists_hasSexticRoot_iff: a separable integral resolvent sextic has a rational root exactly when it has the integral root required by resolvent evidence.

theorem TauCeti.exists_hasSexticRoot_iff (f : Polynomial ℤ) : (∃ (a : ℤ), HasSexticRoot f a) ↔ (∃ (a : ℚ), (Polynomial.map (Int.castRingHom ℚ) (resolventSextic f)).IsRoot a) ∧ (Polynomial.map (Int.castRingHom ℚ) (resolventSextic f)).Separable

Rational roots of a separable resolvent sextic are exactly its certificate roots. Since the resolvent sextic is monic over ℤ, the integral root theorem shows that every rational root is an integer. Thus a separable rational resolvent has a root precisely when the integral evidence predicate HasSexticRoot has a witness.