Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Effective count of cone points of idealSet K J with a norm residue

Abstract

Effective count of cone points of idealSet K J with a norm residue.

Theorem 1.1 (Effective count of cone points of idealSet K J with a norm residue).

Lean statement: D5/S3/Arith/PrimeIdeals/NormResidue/IdealCongruenceCountCells.exists_card_idealSet_residue_le

Proof. Machine-checked in Lean as D5/S3/Arith/PrimeIdeals/NormResidue/IdealCongruenceCountCells.exists_card_idealSet_residue_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.

Effective count of cone points of idealSet K J with a norm residue (the Widmer / GRS geometric core). For a fixed nonzero ideal J, a modulus m and a residue b, the number of cone points a ∈ idealSet K J of mixedEmbedding.norm ≤ N·N(J) whose integer norm intNorm (idealSetEquiv K J a) is ≡ b (mod m) is κ·N + O(N^{1-1/d}), d = [K:ℚ]. This is the substantive analytic input.

References