Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Effective residue count in an orthant cell

Abstract

Effective residue count in an orthant cell.

Theorem 1.1 (Effective residue count in an orthant cell).

Lean statement: D5/S3/Arith/PrimeIdeals/NormResidue/IdealCongruenceCountCellGeometry.exists_card_residue_fibre_sub_mul_rpow_le_explicit

Proof. Machine-checked in Lean as D5/S3/Arith/PrimeIdeals/NormResidue/IdealCongruenceCountCellGeometry.exists_card_residue_fibre_sub_mul_rpow_le_explicit (✓ std3). ∎

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

Commentary.

Fix a real-sign orthant and a lattice coset. The number of cone points in that cell with a prescribed norm residue differs from its explicit volume term by at most C times the dilation to degree d - 1. The leading term is zero when the cell does not carry the prescribed residue.

References