Three-Saturation of a Pure Cubic Order
Abstract
Trace integrality excludes denominator three in a pure cubic suborder.
Theorem 1.1 (Integral elements with a triple in the order).
Lean statement: D5/S3/Arith/Lattices/PureCubicThreeSaturation.pure_cubic_three_saturation
Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/PureCubicThreeSaturation.pure_cubic_three_saturation (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let K have a rational cubic power basis generated by theta, with theta cubed equal to 1 + 9a for an integer a. Put beta = (1 + theta + theta squared)/3. An element of K is in the displayed order when it is an integer linear combination of 1, theta, and beta.
If z is integral and three times z is in this order, then z itself is in the order. Writing three times z in the displayed basis, the integral traces of z, the square of z after removing its beta term, and the cube after also removing its constant term force each of the three coefficients to be divisible by three.
The theorem controls the prime three in the normalization problem. Primes dividing the radicand require separate local arguments.