10. Main Theorem
Theorem. The prime race constant \varrho = \sum_{k \ge 0} b_k\,2^{-(k+1)} — the number
whose binary expansion is 0.b_0 b_1 b_2 \ldots_2, where b_k = 1 exactly when the
k-th odd prime is \equiv 3 \pmod 4 — is irrational.
Lean code for Theorem irrational_ϱ
-
⟲
theorem irrational_ϱ : Irrational ϱ
theorem irrational_ϱ : Irrational ϱ
Pure logic; no new mathematics. If \varrho were rational, its bit sequence would be
eventually periodic; eventual periodicity would force the race sum onto a linear trajectory
|S(N) - c\,\pi(N)| \le C; and the main analytic theorem says no such trajectory exists.
\blacksquare
⟲by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.
by_contra`by_contra h` proves `⊢ p` by contradiction,
introducing a hypothesis `h : ¬p` and proving `False`.
* If `p` is a negation `¬q`, `h : q` will be introduced instead of `¬¬q`.
* If `p` is decidable, it uses `Decidable.byContradiction` instead of `Classical.byContradiction`.
* If `h` is omitted, the introduced variable will be called `this`.
* `h` can be any pattern supported by `rcases`/`rintro`.
h¬Irrational ϱ
exact`exact e` closes the main goal if its target type matches that of `e`.
raceSum_not_linearA362583.raceSum_not_linear : ¬∃ c C, ∀ (N : ℕ), |↑(raceSum N) - c * ↑N.primeCounting| ≤ C**Main analytic theorem**: the mod-4 prime race is never linear — there are no
constants `c`, `C` with `|S(N) - c·π(N)| ≤ C` for all `N`, where `S = raceSum` and
`π = Nat.primeCounting` (# primes `≤ N`).
Case `c ≠ 0` is `c_eq_zero_of_raceSum_linear`; case `c = 0` reduces to the bounded-race
hypothesis `|S(N)| ≤ C`. The continued logarithm `contLog` satisfies
`exp ∘ contLog = L(χ, ·)` on `Ω = {Re s > 1/2}` by the identity theorem
(`norm_LFunction_eq_exp_re_contLog`), but `Re (contLog σ) ≥ layerBReal σ - C - cT → ∞` as
`σ ↓ 1/2` by divergence transfer (`layerBReal_sub_le_re_contLog` + `exists_layerBReal_gt`),
contradicting the continuity of the entire `L(χ, ·)` at `1/2`
(`exists_norm_LFunction_lt_near_half`) — evaluated at a single point `σ*`, with no filters.
(raceSum_linear_of_eventuallyPeriodicA362583.raceSum_linear_of_eventuallyPeriodic :
(∃ N P, 0 < P ∧ ∀ k ≥ N, bit (k + P) = bit k) → ∃ c C, ∀ (N : ℕ), |↑(raceSum N) - c * ↑N.primeCounting| ≤ CAn eventually periodic bit sequence makes
the race sum linear in the prime count, `raceSum N = c·π(N) + O(1)`. The slope
is `c = W/P` for the exact window sum `W = ∑_{k∈[N₀,N₀+P)} (1 - 2·bit k) = P - 2j`,
and the constant `C = 2·N₀ + 2·P + 1` absorbs the `m = π(N) - 1` reindexing
via `|c| ≤ 1` (all-ones/all-zeros patterns are just `c = ∓1`, no separate case). (eventuallyPeriodic_of_not_irrationalA362583.eventuallyPeriodic_of_not_irrational : ¬Irrational ϱ → ∃ N P, 0 < P ∧ ∀ k ≥ N, bit (k + P) = bit kIf `ϱ` is rational, its bit sequence is
eventually periodic — pigeonhole two equal tails `t m = t n` (`exists_t_collision`),
propagate the collision by the recurrence's determinism (`t_eq_add`), giving period
`P = n - m` from index `m`. h¬Irrational ϱ))
What has been proved, precisely: the irrationality of \varrho above — a statement mentioning
only the n-th-prime function, remainder arithmetic, finite sums, and one convergent
series. Its analytic core, the non-linearity of the mod-4 prime race (the main analytic
theorem of the Nonlinearity of the Prime Race chapter), is proved in full and quantifies
over the same elementary objects. Both are sorry-free, and that is checked rather than
asserted: building this site runs collectAxioms over every declaration it presents and over
every declaration named in formalization.yaml, and the build fails if an axiom closure falls
outside propext, Classical.choice, Quot.sound. sorryAx is an axiom for that purpose, so the
same check also rules out a sorry reached through a dependency, not only one written here.
Mathlib is pinned at toolchain v4.32.0.
The analytic footprint stayed as small as promised in the Introduction: the continued
L(s, \chi_4) and its entirety, L(1, \chi_4) \ne 0, the exponential Euler product, the
divergence of \sum_p 1/p (used exactly twice, both inside the divergence transfer), and
the identity theorem. Three features of the Lean proof: the by-parts series
defined as the continuation, the per-prime split instead of a double-sum rearrangement, and
single-point contradictions in both cases.
The Lean sources and this blueprint are released under the Apache License 2.0.