Registry · Theorem I.T52 tau-effective formalized

I.T52 — Bias at Primorial Levels

Chebyshev bias at primorial levels: at each M_k (capped at 50), the bias for (q=4, 3 vs 1) is non-negative. Non-residues lead at each primorial stage. Connects to B/C sector asymmetry. Verified at depth 3.

Book I Part 5 Ch. 30

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookI.Coordinates.ChebyshevBias

Symbol: bias_primorial_3