Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Cubic Inertia and Signature

Abstract

Local inertia and signature of actual golden cubic fields.

Theorem 1.1 (Primes over three and conjugation).

Lean statement: D5/S3/Factorization/Galois/GoldenCubicCommonInertiaAndSignature.actual_common_cubic_three_prime_orbits

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/GoldenCubicCommonInertiaAndSignature.actual_common_cubic_three_prime_orbits (✓ std3). ∎

Source. Repository-derived.

Commentary.

The actual common field of J golden blocks has three to the J primes above the rational prime three. Each has absolute ramification index two and residue degree one. Actual complex conjugation fixes exactly one of these primes.

Theorem 1.2 (Inertia fixes unit radical coordinates).

Lean statement: D5/S3/Factorization/Galois/GoldenCubicCommonInertiaAndSignature.actual_common_cubic_inertia_unit_coordinates

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/GoldenCubicCommonInertiaAndSignature.actual_common_cubic_inertia_unit_coordinates (✓ std3). ∎

Source. Repository-derived.

Commentary.

At a prime above a rational prime other than three, every inertia automorphism fixes the cubic root of unity. It also fixes each chosen positive cube root whose cube-free residue is a unit at that rational prime, for indices from one through J.

Theorem 1.3 (Inertia bound on the block support).

Lean statement: D5/S3/Factorization/Galois/GoldenCubicCommonInertiaAndSignature.actual_common_cubic_inertia_card_le_three

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/GoldenCubicCommonInertiaAndSignature.actual_common_cubic_inertia_card_le_three (✓ std3). ∎

Source. Repository-derived.

Commentary.

When a rational prime other than three divides one of the first J golden blocks, the inertia group at a prime of the common field above it has at most three elements. Distinct block supports force all other radical coordinates to be fixed.

Theorem 1.4 (Degrees and signature of actual fields).

Lean statement: D5/S3/Factorization/Galois/GoldenCubicCommonInertiaAndSignature.actual_common_cubic_rational_degree_and_signature

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/GoldenCubicCommonInertiaAndSignature.actual_common_cubic_rational_degree_and_signature (✓ std3). ∎

Source. Repository-derived.

Commentary.

The rational field generated by the first J positive golden cubic roots has degree three to the J. Adding the cubic root of unity gives a field of twice that degree. The positive-root field is a number field with one real place and (3^J - 1)/2 complex places.

References