Mixed Pure Cubic Integer Ring
Abstract
The mixed cubic lattice is the integer ring, with field discriminant minus three times the square of mn.
Theorem 1.1 (Maximality and field discriminant).
Lean statement: D5/S3/Arith/Lattices/PureCubicMixedMaximality.pure_cubic_mixed_maximality_and_discriminant
Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/PureCubicMixedMaximality.pure_cubic_mixed_maximality_and_discriminant (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let K be a cubic number field with a rational power basis generated by alpha. Let m and n be positive, squarefree, and coprime integers, with alpha cubed equal to m times n squared. Choose integers c, a, k, and v such that v is one or minus one, c cubed times m n squared is one plus nine a, and c squared times n is v plus three k. Put beta = alpha squared divided by n, gamma = (1 + c alpha + v beta)/3, and let S be the integer span of 1, alpha, and gamma.
Every element of K integral over the integers lies in S. Conversely, all three generators of S are integral, so S is the full ring of integers. Its field discriminant is -3(mn) squared.
To remove a factor of three from an integral element, scale alpha to theta = c alpha. The cubic equation theta cubed = 1 + 9a gives a three-saturated lattice generated by 1, theta, and (1 + theta + theta squared)/3. Explicit lattice inclusions and Bezout’s identity transfer that saturation to S. At any other prime dividing the power-basis discriminant, squarefreeness and coprimality select one of the two mixed-radicand prime-saturation cases. Discriminant clearing followed by prime removal puts every integral element in S. Integral coordinate changes between this basis and an integral basis identify its trace discriminant with the field discriminant.