Seven-adic certificates for the level-seven CM loci

The quadratic t² + 245t + 2401 and the quartic t⁴ - 490t³ - 21609t² - 235298t - 823543 cut out the complex multiplication fibres (over j = 0 and j = 1728) of the degeneracy loci of level-seven hauptmodul correspondences. Neither has a rational root: the quadratic dies modulo eight and the quartic modulo five. Both facts are shared by the X₀(21) and X₀(49) transfer files.

theorem MazurTorsion.levelSevenQuadratic_ne_zero (t₇ : ℚ) : t₇ ^ 2 + 245 * t₇ + 2401 ≠ 0

The quadratic factor t₇² + 245t₇ + 2401 has no rational root.

theorem MazurTorsion.levelSevenQuartic_ne_zero (t₇ : ℚ) : t₇ ^ 4 - 490 * t₇ ^ 3 - 21609 * t₇ ^ 2 - 235298 * t₇ - 823543 ≠ 0

The quartic factor has no rational root.