An odd prime missing the cubic discriminant misses the index
ProvedCollapsibleCubics.not_dvd_index_of_not_dvd_cubicDiscralgebraic-number-theorynumber-theory
Let with irreducible over , let be the resulting cubic field and the root. Let be an odd prime not dividing the discriminant . Then does not divide the index .
This is the index-discriminant relation specialised to the cubic: since the index squared divides , any prime missing misses the index.
Preamble
import Mathlib import Definitions.Def_CollapsibleCubics_q7
Formal statement
namespace CollapsibleCubics
open NumberField
theorem not_dvd_index_of_not_dvd_cubicDiscr (D E : ℤ)
[Fact (Irreducible (cubicPoly (D : ℚ) (E : ℚ)))] {p : ℕ} (hp : p.Prime) (hodd : Odd p)
(hnd : ¬ (p : ℤ) ∣ (-4 * D ^ 3 - 27 * E ^ 2)) :
¬ p ∣ (adjoinAddSubgroup (thetaO D E)).index := by sorry
end CollapsibleCubicsSource
Collapsible Cubics mission (Q7 support chain); proved in the project repo, restated here for the platform. Background: https://quesswho.github.io/miles-blog/2026/08/20/collapsible/