A362583 Irrationality
The prime race constant \varrho is the sum of the series
\varrho \;=\; \sum_{k \ge 0} \frac{b_k}{2^{\,k+1}} \;=\; 0.7004001\ldots,
which converges absolutely by comparison with the geometric series. Since each b_k is
0 or 1, the series is exactly the place-value reading of the binary numeral
0.b_0 b_1 b_2 \ldots_2 — and these are genuinely the binary digits of \varrho:
infinitely many b_k are 0 (Dirichlet's theorem), so the digit string is not
eventually all 1s and no carry ambiguity arises. Reading successive digit prefixes as
binary integers recovers the OEIS sequence A362583, which is why we call \varrho the
A362583 constant. The theorem of this blueprint is that \varrho is irrational.
Lean code for Definition ϱ
-
⟲
def ϱ : ℝ
Real : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.def ϱ : ℝ
Real : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.
⟲:= ∑' kℕ : ℕNat : TypeThe natural numbers, starting at zero.
This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
, (bitA362583.bit (k : ℕ) : ℕ`k`-th bit of the constant: `1` iff the `k`-th odd prime is `≡ 3 (mod 4)`.
The `b_{k+1}` of the 1-based bit sequence; first values `1 0 1 1 0 0 1 1`
(primes `3, 5, 7, 11, 13, 17, 19, 23`). kℕ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) / 2ℝ ^ (kℕ + 1ℕ)
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 ϱ))