Part of: The main theorem: the prime race constant is irrational.
Theoremirrational_ϱ
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
Irrational (x : ℝ) : PropA real number is irrational if it is not equal to any rational number.ϱA362583.ϱ : ℝThe prime race constant (the A362583 constant): the sum of the series `ϱ = Σ_{k ≥ 0} bit k · 2^{-(k+1)}`, i.e. the real number whose `k`-th binary digit is `bit k` — in binary `0.b₀b₁b₂…₂ ≈ 0.7004001…` (decimal). OEIS A362583 lists the successive digit prefixes read as binary integers.theorem irrational_ϱ : Irrational
Irrational (x : ℝ) : PropA real number is irrational if it is not equal to any rational number.ϱA362583.ϱ : ℝThe prime race constant (the A362583 constant): the sum of the series `ϱ = Σ_{k ≥ 0} bit k · 2^{-(k+1)}`, i.e. the real number whose `k`-th binary digit is `bit k` — in binary `0.b₀b₁b₂…₂ ≈ 0.7004001…` (decimal). OEIS A362583 lists the successive digit prefixes read as binary integers.
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 ϱ))