Real Fifth-Cyclotomic Subfield

Abstract

The real fifth-cyclotomic generator and root five generate the same field.

Theorem 1.1 (The real fifth-cyclotomic field is generated by root five).

$$\mathbb{Q}⟨2\cos (2\pi /5)⟩=\mathbb{Q}⟨\sqrt{5}⟩.$$

Proof. Machine-checked in Lean as D5/S3/Constants/Cyclotomy/RealSubfield.real_cyclotomic_generator_adjoin_eq_sqrt_five (✓ std3). ∎

Source. Repository-derived.

Commentary.

The existing pentagon identity identifies the real generator 2 cos(2 pi / 5) with (sqrt(5) - 1) / 2. Field closure therefore places this generator in Q(sqrt(5)); conversely, rearranging the identity as sqrt(5) = 2 times the generator plus 1 places sqrt(5) in the field generated by the cosine. The two inclusions give equality.

This closes only the sentence Q(zeta_5)^+ = Q(sqrt(5)) from clause 2, using its standard real-generator presentation by 2 cos(2 pi / 5). It does not claim closure of the clause’s other three welding assertions.

References

• Truth anchor: D5/S3/Constants/Cyclotomy/RealSubfield.real_cyclotomic_generator_adjoin_eq_sqrt_five
• Dependency: D5/S3/Constants/PentagonCosines