Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Effective product-ideal residue fibre count

Abstract

Effective product-ideal residue fibre count.

Theorem 1.1 (Effective product-ideal residue fibre count).

Lean statement: D5/S3/Arith/PrimeIdeals/NormResidue/IdealCongruenceCountDvdFibre.exists_card_fibre_dvd_residue_sub_mul_rpow_le

Proof. Machine-checked in Lean as D5/S3/Arith/PrimeIdeals/NormResidue/IdealCongruenceCountDvdFibre.exists_card_fibre_dvd_residue_sub_mul_rpow_le (✓ 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 each sign orthant and lattice coset, the product-ideal residue fibre count has a leading cell volume term divided by the norm of the additional ideal, with an error bounded by a constant times the dilation to degree d - 1. The leading term vanishes when the original cell does not carry the residue.

References