Examples of quintic Galois-group certificate evidence

This module gives a symmetric-route certificate for X⁵ - X - 1, from its factorizations modulo 5 and 2, and reads the label 5T5 off it.

Main results

• TauCeti.QuinticCertificate.check_symmetric_X_pow_five_sub_X_sub_one: X⁵ - X - 1 has a symmetric-route certificate.
• TauCeti.hasGaloisLabel_X_pow_five_sub_X_sub_one: X⁵ - X - 1 has label 5T5.

theorem TauCeti.QuinticCertificate.check_symmetric_X_pow_five_sub_X_sub_one : (symmetric 5 2).check (Polynomial.X ^ 5 - Polynomial.X - 1) = true

X⁵ - X - 1 has a symmetric-route certificate: it is irreducible modulo 5, and has factor degrees (2,3) modulo 2. Both primes are good, since neither divides its discriminant.

theorem TauCeti.hasGaloisLabel_X_pow_five_sub_X_sub_one : HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) (Polynomial.X ^ 5 - Polynomial.X - 1)) ⟨4, hasGaloisLabel_X_pow_five_sub_X_sub_one._proof_1⟩

X⁵ - X - 1 has label 5T5. Its symmetric-route certificate checks.