Registry · Definition I.D102 tau-effective formalized

I.D102 — Chebyshev Bias Measure

Chebyshev bias B(x; q, a₁, a₂): count how often π(n;q,a₁) > π(n;q,a₂) for n ≤ x. For (q=4, 3 vs 1), bias is positive up to x=50: non-residues lead more often. Quantifies prime race advantage.

Book I Part 5 Ch. 30

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookI.Coordinates.ChebyshevBias

Symbol: chebyshev_bias