Registry · Definition I.D101 established formalized

I.D101 — Prime Counting in Progressions

π(x; q, a) counts primes p ≤ x with p ≡ a (mod q). For q=4: π(x;4,3) typically exceeds π(x;4,1). For q=3: π(x;3,2) exceeds π(x;3,1). Reflects quadratic residue structure.

Book I Part 5 Ch. 30

Dependency Graph

Depends on (1)

Depended on by (2)

Lean Formalization

Module: TauLib.BookI.Coordinates.ChebyshevBias

Symbol: prime_count_mod