Cubic Radical Towers from Base-Field Tests
Abstract
Saturated tests in a field containing the cube roots of unity certify the degree of a finite cubic radical tower.
Theorem 1.1 (Every cubic radical stage has degree three).
Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/CubicRadicalTowerDegree.cubic_radical_tower_degree_of_saturated_noncube_tests (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let K be a field containing a primitive cube root of unity and let L be an extension field. Fix a natural number J and base elements a_j with specified cube roots beta_j in L for indices one through J. The intermediate field K_m is generated by the first m roots; K_0 is K.
For each n from zero through J, a predicate P_n on K accepts no cube and is preserved when an accepted element is multiplied by any nonnegative power of any a_i with one less than or equal to i less than or equal to n. For n strictly less than J the test also accepts a_(n+1). These assumptions imply that the degree of K_J over K is 3^J and that any element accepted by P_J still has no cube root in K_J. No additional assumption that the radicands are nonzero is needed: zero is a cube and is excluded by each fresh test.
Cubic descent proves that a cube root appearing in a later stage would turn a tested element times a power of that stage’s radicand into a cube in the preceding field. Preservation of the base-field test excludes this possibility by induction. Consequently each polynomial T^3-a_j is irreducible over the preceding stage, and multiplication of the stage degrees gives the degree formula and the terminal noncube statement. The empty tower has degree one and retains the base-field test.
Valuations whose integer logarithms are nonzero modulo three can supply these tests when earlier radicands have valuation one. Their required values must be established for the actual radicands. The degree formula alone gives no Frobenius coordinates, cyclotomic intersection, density, or discriminant formula.
Theorem 1.2 (Diagonal valuations and a retained noncube unit).
Lean statement: D5/S3/Factorization/Galois/CubicRadicalTowerDegree.finite_valuation_degree_and_unit_noncube
Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/CubicRadicalTowerDegree.finite_valuation_degree_and_unit_noncube (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let finitely many nonzero radicands over a field have specified cube roots. For each radicand, choose a valuation whose integer logarithm there is not divisible by three and whose value on every other radicand is one.
If the base field contains a primitive cube root of unity, the generated radical field has degree three to the number of radicands. A base-field unit that is not a cube and has valuation logarithm zero at all chosen valuations remains a noncube in that generated field.