Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

the degree-≥ 2 part of T vanishes in the density ratio

Abstract

the degree-≥ 2 part of T vanishes in the density ratio.

Theorem 1.1 (the degree-≥ 2 part of T vanishes in the density ratio).

Lean statement: D5/S3/Factorization/Galois/Chebotarev/FixedFieldHigherDegreeTail.primeIdealZetaSum_T2_div_univ_tendsto_zero

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

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

Commentary.

For T₂ defined as the fixed-field Frobenius set after removing degree-one primes over K unramified in L, the partial prime sum over T₂ divided by the universal prime sum over E tends to zero as s decreases to one from above. The higher-degree part is bounded above by a convergent square-power prime sum; primes lying above the finitely many ramified base primes contribute a finite remainder.

References