Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Completions and Conjugation of Golden Cubic Fields

Abstract

Completions at three and rational conjugation for the actual common golden cubic fields.

Theorem 1.1 (Completions above three).

Lean statement: D5/S3/Factorization/Galois/GoldenCubicCommonCompletionAndGalois.actual_common_cubic_three_completion_collapses

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

Source. Repository-derived.

Commentary.

For every initial segment of the actual golden cubic tower, take a prime of its cubic cyclotomic base above three and any prime of the tower above it. The base and tower are number fields. There is a continuous surjective ring homomorphism between their adic completions that agrees with the two embeddings of the base field.

Theorem 1.2 (Relative ramification above three).

Lean statement: D5/S3/Factorization/Galois/GoldenCubicCommonCompletionAndGalois.actual_common_cubic_three_completion_and_ramification

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

Source. Repository-derived.

Commentary.

For the same primes above three, the compatible continuous surjection of completions forces the ramification index of the tower over its cubic cyclotomic base to equal one. The completion map is retained in the conclusion together with that index.

Theorem 1.3 (Relative residue degree above three).

Lean statement: D5/S3/Factorization/Galois/GoldenCubicCommonCompletionAndGalois.actual_common_cubic_three_residue_degree_one

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

Source. Repository-derived.

Commentary.

At every prime of the actual tower over a prime of the cubic cyclotomic base above three, the residue field extension has degree one. The proof uses the compatible completion map to approximate integral residues.

Theorem 1.4 (Rational Galois action and conjugation).

Lean statement: D5/S3/Factorization/Galois/GoldenCubicCommonCompletionAndGalois.actual_common_cubic_q_galois_and_conjugation

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

Source. Repository-derived.

Commentary.

The actual common field of J golden blocks is Galois over the rationals. Complex conjugation restricts to a nonidentity automorphism of order two on this field. It conjugates each automorphism over the cubic cyclotomic base to its inverse.

Theorem 1.5 (Normalizer of conjugation).

Lean statement: D5/S3/Factorization/Galois/GoldenCubicCommonCompletionAndGalois.actual_common_cubic_conjugation_self_normalizing

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

Source. Repository-derived.

Commentary.

The order-two subgroup generated by actual complex conjugation is its own normalizer in the rational automorphism group of the common golden cubic field. The conclusion identifies the automorphism through its action on the designated complex embedding.

References