An alternating quintic certificate

The polynomial X⁵ + 20X - 16 has discriminant 32000², is irreducible modulo 3, and has factor degrees (1,1,3) modulo 7. These data give an alternating-route certificate, proving that its Galois group over ℚ has label 5T4.

The main results are TauCeti.QuinticCertificate.check_X_pow_five_add_twenty_mul_X_sub_sixteen and TauCeti.hasGaloisLabel_X_pow_five_add_twenty_mul_X_sub_sixteen.

theorem TauCeti.discr_X_pow_five_add_twenty_mul_X_sub_sixteen : (Polynomial.X ^ 5 + 20 * Polynomial.X - 16).discr = 32000 ^ 2

The discriminant of X⁵ + 20X - 16 is 32000².

theorem Polynomial.irreducible_X_pow_five_add_twenty_mul_X_sub_sixteen_zmod_three : Irreducible (X ^ 5 + 20 * X - 16)

The reduction of X⁵ + 20X - 16 modulo 3 is irreducible.

@[simp]

theorem Polynomial.factorDegrees_X_pow_five_add_twenty_mul_X_sub_sixteen_three : (X ^ 5 + 20 * X - 16).factorDegrees 3 = {5}

The alternating quintic has a single irreducible factor of degree five modulo 3.

theorem Polynomial.instFactPrimeOfNatNat_tauCeti : Fact (Nat.Prime 7)

@[simp]

theorem Polynomial.factorDegrees_X_pow_five_add_twenty_mul_X_sub_sixteen_seven : (X ^ 5 + 20 * X - 16).factorDegrees 7 = {1, 1, 3}

The reduction of X⁵ + 20X - 16 modulo 7 has factor degrees {1, 1, 3}.

@[simp]

theorem TauCeti.QuinticCertificate.check_X_pow_five_add_twenty_mul_X_sub_sixteen : (alternating 3 7 32000).check (Polynomial.X ^ 5 + 20 * Polynomial.X - 16) = true

The alternating-route certificate for X⁵ + 20X - 16 checks, using primes 3 and 7 and the square root 32000 of its discriminant.

theorem TauCeti.hasGaloisLabel_X_pow_five_add_twenty_mul_X_sub_sixteen : HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) (Polynomial.X ^ 5 + 20 * Polynomial.X - 16)) ⟨3, hasGaloisLabel_X_pow_five_add_twenty_mul_X_sub_sixteen._proof_1⟩

X⁵ + 20X - 16 has Galois label 5T4.