Cyclotomic

Abstract

Cyclotomic.

Theorem 1.1 (Cyclotomic).

Lean statement: D5/S3/Factorization/Galois/Chebotarev/Cyclotomic.cyclotomic_density_from_two_sided_asymp

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/Chebotarev/Cyclotomic.cyclotomic_density_from_two_sided_asymp (✓ std3). ∎

Citation. Chris Birkbeck and the Chebotarev density contributors (2026). Chebotarev density in Lean. URL: https://github.com/CBirkbeck/chebotarev-density/tree/a00054a0e6bbc394b0e81de750db0cd2efc8bd88.

Commentary.

Sharifi 7.2.1 step (iv) — two-sided log-asymptotic comparison (p. 142). Source: “on the one hand we have Σ_χ χ(σ)^{-1} log L(χ,s) ~ |G| Σ_{φ_𝔭=σ} N𝔭^{-s}, whereas on the other we have Σ_χ χ(σ)^{-1} log L(χ,s) ~ log ζ_K(s) ~ log(s-1)^{-1}”. Comparing yields density 1/|G|.

References

• Truth anchor: D5/S3/Factorization/Galois/Chebotarev/Cyclotomic.cyclotomic_density_from_two_sided_asymp
• Dependency: D5/S3/Analytic/Zeta/NumberField/ZetaProduct
• Dependency: D5/S3/Factorization/Galois/Chebotarev/CyclotomicCharacterBounds
• Dependency: D5/S3/Factorization/Galois/Chebotarev/CyclotomicNormResidue