1. Introduction🔗

The subject of this blueprint is a single real number. List the odd primes in order — 3, 5, 7, 11, 13, 17, 19, 23, \ldots — and record one binary digit for each: b_k = 1 if the k-th odd prime is congruent to 3 modulo 4, and b_k = 0 if it is congruent to 1. Reading the digits as a binary expansion produces the prime race constant \varrho, the constant of Vergo (2023), \varrho \;=\; 0.10110011\ldots_2 \;=\; \sum_{k \ge 0} b_k\, 2^{-(k+1)} \;\approx\; 0.7004, and this site documents a complete, sorry-free Lean 4 proof of the theorem that \varrho is irrational.

The digits of \varrho transcribe the mod-4 prime race. Chebyshev observed in 1853 that primes \equiv 3 \pmod 4 appear to lead primes \equiv 1 \pmod 4 most of the time, and the race sum S(N) = \sum_{p \le N} \chi_4(p) — where \chi_4 is the nonprincipal character mod 4, so each prime \equiv 1 scores +1 and each prime \equiv 3 scores -1 — is the classical measure of that bias. Irrationality of \varrho says the race never settles into an eventually periodic pattern of leads and deficits: the sequence of residues is, in this precise sense, aperiodic forever.

The argument combines four results:

• Both residue classes 1, 3 \bmod 4 contain infinitely many primes (Dirichlet's theorem at modulus 4), so the digit sequence has infinitely many zeros and infinitely many ones.

• If \varrho were rational, its digit sequence would be eventually periodic — a self-contained tail-and-pigeonhole argument that avoids any general theory of digit expansions.

• Eventually periodic digits force the rigid conclusion S(N) = c\,\pi(N) + O(1) for a rational slope c, where \pi(N) counts the primes \le N.

• No such linear race exists: the main analytic theorem, that the mod-4 race sum is never c\,\pi(N) + O(1).

Only the last result is analytically deep, and its difficulty is bounded sharply. The classical irrationality routes for constants of this kind run through Littlewood's 1914 \Omega_\pm-oscillation for the race, or through long runs of consecutive primes in a fixed class — both far beyond current formalization technology. Neither is needed: refuting the linear trajectory requires only non-degeneracy of the race, not quantitative oscillation. The analytic inputs are exactly five, all present in Mathlib: the analytically continued Dirichlet L-function L(s, \chi_4), its nonvanishing at s = 1, the exponential form of the Euler product, the divergence of \sum_p 1/p, and the identity theorem for holomorphic functions. No prime number theorem, no PNT in arithmetic progressions, no zero-free regions, no functional equation.

A statement-hygiene principle governs the Lean development: the four definitions, the irrationality theorem, and the analytic core it rests on mention only elementary objects — the k-th prime, remainder arithmetic, finite sums, and one geometric-type series — so a reader can audit what was proved without trusting any of the analytic machinery, which is confined to proofs. The chapters that follow develop the full argument in the order the Lean sources prove it: the digit combinatorics, the layer decomposition of the Euler-product logarithm, and the two-case refutation of a linear race.