Liouville criterion

variant-1629563f

proved

Restated as hole h_liouville of erdos-257 (split by 20261023T133841Z-t1023-f1-partial.lean).

$\displaystyle \forall A \subseteq \mathbb{N}:\quad A \text{ infinite},\ 0 \notin A,\ \Bigl(\forall C \in \mathbb{N}\ \exists m \in A\ \exists L \in \mathbb{N}:\ L > 0,\ \bigl(\forall a \in A,\ a < m \Rightarrow (2^a - 1) \mid L\bigr),\ 2^C L \le 2^m\Bigr) \ \Longrightarrow\ \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

In the hypothesis $2^a - 1$ is subtraction on natural numbers, which never truncates here since $2^a \ge 1$. The sum is over the elements of $A$; $0 \notin A$ excludes Lean's junk value at $n = 0$.

The docstring's example $\{2^k - 1\}$ is to be read with $k \ge 1$: at $k = 0$ it contains $0$, which the hypothesis $0 \notin A$ excludes.

(The last paragraph is t1022-k's, from t1022-n's review; the rest is t1022-b's.)

unverified · history

Lean

theorem Opn.erdos_257_liouville_criterion :
    ∀ (A : Set ℕ), A.Infinite → 0 ∉ A →
    (∀ C : ℕ, ∃ m ∈ A, ∃ L : ℕ, 0 < L ∧ (∀ a ∈ A, a < m → 2 ^ a - 1 ∣ L) ∧ 2 ^ C * L ≤ 2 ^ m) →
    Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := by
  sorry

Why does it end in sorry?

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

How it was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000903, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000903.json, merge commit 826790afe881.

Outline of Proof.lean, extracted by the gate at 1bd7ca70c9ee from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

hsum have Summable (A.indicator fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)))
Leaves False, with hsum : Summable (A.indicator fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))).
Uses library Summable.
Lean, lines 89–90
```
  have hsum : Summable (A.indicator (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1))) :=
    lac_summable.indicator A
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 89–90 at 826790afe881 ↗
hrA have (↑r : ℝ) = ∑' (n : ℕ), A.indicator (fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) n
Leaves False, with hrA : (↑r : ℝ) = ∑' (n : ℕ), A.indicator (fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) n.
Uses library tsum_subtype.
Lean, lines 91–92
```
  have hrA : (r : ℝ) = ∑' n, A.indicator (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) n :=
    hr.trans (tsum_subtype A (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)))
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 91–92 at 826790afe881 ↗
s3 obtain ∃ m ∈ A, ∃ (L : ℕ), (0 : ℕ) < L ∧ (∀ a ∈ A, a < m → (2 : ℕ) ^ a - (1 : ℕ) ∣ L) ∧ (2 : ℕ) ^ ((4 : ℕ) * q) * L ≤ (2 : ℕ) ^ m
Leaves False, with m : ℕ, hmA : m ∈ A, L : ℕ, hL0 : (0 : ℕ) < L, hLdvd : ∀ a ∈ A, a < m → (2 : ℕ) ^ a - (1 : ℕ) ∣ L, hLm : (2 : ℕ) ^ ((4 : ℕ) * q) * L ≤ (2 : ℕ) ^ m.
Lean, line 94
```
  obtain ⟨m, hmA, L, hL0, hLdvd, hLm⟩ := hA (4 * q)
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 94 at 826790afe881 ↗
hm1 have (1 : ℕ) ≤ m
Leaves False, with hm1 : (1 : ℕ) ≤ m.
Uses library Nat.eq_zero_or_pos.
Lean, lines 95–98
```
  have hm1 : 1 ≤ m := by
    rcases Nat.eq_zero_or_pos m with h | h
    · exact absurd (h ▸ hmA) h0
    · exact h
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 95–98 at 826790afe881 ↗
1. hm1.s1 case
  Leaves (1 : ℕ) ≤ m, with h : m = (0 : ℕ).
  Uses library absurd.
  Lean, line 97
  · exact absurd (h ▸ hmA) h0
  targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 97 at 826790afe881 ↗
2. hm1.s2 case
  Leaves (1 : ℕ) ≤ m, with h : m > (0 : ℕ).
  Lean, line 98
  · exact h
  targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 98 at 826790afe881 ↗
hsplit have ∑ i ∈ Finset.range m, A.indicator (fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) i + ∑' (i : ℕ), A.indicator (fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) (i + m) = ∑' (i : ℕ), A.indicator (fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) i
Leaves False, with hsplit : ∑ i ∈ Finset.range m, A.indicator (fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) i + ∑' (i : ℕ), A.indicator (fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) (i + m) = ∑' (i : ℕ), A.indicator (fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) i.
Lean, line 100
```
  have hsplit := hsum.sum_add_tsum_nat_add m
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 100 at 826790afe881 ↗
hfin have ∑ i ∈ Finset.range m, A.indicator (fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) i = ∑ a ∈ F, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ))
Leaves False, with hfin : ∑ i ∈ Finset.range m, A.indicator (fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) i = ∑ a ∈ F, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)).
Uses library Finset.range, Finset.sum_filter, Set.indicator_apply.
Lean, lines 101–104
```
  have hfin : ∑ i ∈ Finset.range m, A.indicator (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) i
      = ∑ a ∈ F, (1 : ℝ) / (2 ^ a - 1) := by
    rw [hF, Finset.sum_filter]
    simp [Set.indicator_apply]
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 101–104 at 826790afe881 ↗
hTs have Summable fun (i : ℕ) => A.indicator (fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) (i + m)
Leaves False, with hTs : Summable fun (i : ℕ) => A.indicator (fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) (i + m).
Uses library Summable, summable_nat_add_iff.
Lean, lines 106–107
```
  have hTs : Summable (fun i => A.indicator (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) (i + m)) :=
    (summable_nat_add_iff m).mpr hsum
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 106–107 at 826790afe881 ↗
hTpos have (0 : ℝ) < T
Leaves False, with hTpos : (0 : ℝ) < T.
Uses library Summable.tsum_pos, Set.indicator_nonneg, zero_add, Set.indicator_of_mem, div_pos, one_pos.
Lean, lines 108–112
```
  have hTpos : 0 < T := by
    apply Summable.tsum_pos hTs (fun i => Set.indicator_nonneg (fun n _ => lac_f_nonneg n) _) 0
    rw [zero_add, Set.indicator_of_mem hmA]
    have : (1 : ℝ) < 2 ^ m := one_lt_pow₀ (by norm_num) (by omega)
    apply div_pos one_pos; linarith
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 108–112 at 826790afe881 ↗
1. hTpos.this have (1 : ℝ) < (2 : ℝ) ^ m
  Leaves (0 : ℝ) < (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)), with this : (1 : ℝ) < (2 : ℝ) ^ m.
  Uses library one_lt_pow₀.
  Lean, line 111
  have : (1 : ℝ) < 2 ^ m := one_lt_pow₀ (by norm_num) (by omega)
  targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 111 at 826790afe881 ↗
hTle have T ≤ (4 : ℝ) * (1 / 2 : ℝ) ^ m
Leaves False, with hTle : T ≤ (4 : ℝ) * (1 / 2 : ℝ) ^ m.
Lean, line 113
```
  have hTle : T ≤ 4 * (1 / 2) ^ m := lac_tail_le A m
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 113 at 826790afe881 ↗
hrT have (↑r : ℝ) = ∑ a ∈ F, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) + T
Leaves False, with hrT : (↑r : ℝ) = ∑ a ∈ F, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) + T.
Lean, lines 114–115
```
  have hrT : (r : ℝ) = (∑ a ∈ F, (1 : ℝ) / (2 ^ a - 1)) + T := by
    rw [hrA, ← hsplit, hfin]
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 114–115 at 826790afe881 ↗
s11 obtain ∃ (N : ℤ), (↑L : ℝ) * ∑ a ∈ F, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) = (↑N : ℝ)
Leaves False, with N : ℤ, hN : (↑L : ℝ) * ∑ a ∈ F, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) = (↑N : ℝ).
Uses library Finset.mem_filter, Finset.mem_range.
Lean, lines 116–118
```
  obtain ⟨N, hN⟩ := liou_int L F
    (fun a ha => hLdvd a (Finset.mem_filter.1 ha).2 (Finset.mem_range.1 (Finset.mem_filter.1 ha).1))
    (fun a ha h => h0 (h ▸ (Finset.mem_filter.1 ha).2))
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 116–118 at 826790afe881 ↗
hPpos have (0 : ℝ) < (↑L : ℝ)
Leaves False, with hPpos : (0 : ℝ) < (↑L : ℝ).
Lean, line 119
```
  have hPpos : (0 : ℝ) < L := by exact_mod_cast hL0
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 119 at 826790afe881 ↗
hqr have (↑r : ℝ) * (↑q : ℝ) = (↑r.num : ℝ)
Leaves False, with hqr : (↑r : ℝ) * (↑q : ℝ) = (↑r.num : ℝ).
Uses library Rat.mul_den_eq_num.
Lean, lines 120–121
```
  have hqr : (r : ℝ) * q = r.num := by
    rw [hq]; exact_mod_cast Rat.mul_den_eq_num r
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 120–121 at 826790afe881 ↗
hZ have (↑q : ℝ) * (↑L : ℝ) * T = (↑((↑L : ℤ) * r.num - (↑q : ℤ) * N) : ℝ)
Leaves False, with hZ : (↑q : ℝ) * (↑L : ℝ) * T = (↑((↑L : ℤ) * r.num - (↑q : ℤ) * N) : ℝ).
Lean, lines 122–126
```
  have hZ : (q : ℝ) * L * T = ((L : ℤ) * r.num - q * N : ℤ) := by
    push_cast
    rw [← hN, ← hqr]
    have : T = r - ∑ a ∈ F, (1 : ℝ) / (2 ^ a - 1) := by linarith
    rw [this]; ring
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 122–126 at 826790afe881 ↗
1. hZ.this have T = (↑r : ℝ) - ∑ a ∈ F, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) routine: linarith
  Leaves (↑q : ℝ) * (↑L : ℝ) * T = (↑L : ℝ) * ((↑r : ℝ) * (↑q : ℝ)) - (↑q : ℝ) * ((↑L : ℝ) * ∑ a ∈ F, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ))), with this : T = (↑r : ℝ) - ∑ a ∈ F, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)).
  Lean, line 125
  have : T = r - ∑ a ∈ F, (1 : ℝ) / (2 ^ a - 1) := by linarith
  targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 125 at 826790afe881 ↗
hqpos have (0 : ℝ) < (↑q : ℝ)
Leaves False, with hqpos : (0 : ℝ) < (↑q : ℝ).
Lean, lines 127–128
```
  have hqpos : (0 : ℝ) < q := by
    rw [hq]; exact_mod_cast r.den_pos
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 127–128 at 826790afe881 ↗
hpos have (0 : ℝ) < (↑q : ℝ) * (↑L : ℝ) * T routine: positivity
Leaves False, with hpos : (0 : ℝ) < (↑q : ℝ) * (↑L : ℝ) * T.
Lean, line 129
```
  have hpos : (0 : ℝ) < (q : ℝ) * L * T := by positivity
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 129 at 826790afe881 ↗
hge have (1 : ℝ) ≤ (↑q : ℝ) * (↑L : ℝ) * T
Leaves False, with hge : (1 : ℝ) ≤ (↑q : ℝ) * (↑L : ℝ) * T.
Lean, lines 130–133
```
  have hge : (1 : ℝ) ≤ (q : ℝ) * L * T := by
    rw [hZ] at hpos ⊢
    have : (0 : ℤ) < (L : ℤ) * r.num - q * N := by exact_mod_cast hpos
    exact_mod_cast this
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 130–133 at 826790afe881 ↗
1. hge.this have (0 : ℤ) < (↑L : ℤ) * r.num - (↑q : ℤ) * N
  Leaves (1 : ℝ) ≤ (↑((↑L : ℤ) * r.num - (↑q : ℤ) * N) : ℝ), with this : (0 : ℤ) < (↑L : ℤ) * r.num - (↑q : ℤ) * N.
  Lean, line 132
  have : (0 : ℤ) < (L : ℤ) * r.num - q * N := by exact_mod_cast hpos
  targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 132 at 826790afe881 ↗
hLm' have (2 : ℝ) ^ ((4 : ℕ) * q) * (↑L : ℝ) ≤ (2 : ℝ) ^ m
Leaves False, with hLm' : (2 : ℝ) ^ ((4 : ℕ) * q) * (↑L : ℝ) ≤ (2 : ℝ) ^ m.
Lean, line 134
```
  have hLm' : (2 : ℝ) ^ (4 * q) * L ≤ 2 ^ m := by exact_mod_cast hLm
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 134 at 826790afe881 ↗
hbig have (4 : ℝ) * (↑q : ℝ) < (2 : ℝ) ^ ((4 : ℕ) * q)
Leaves False, with hbig : (4 : ℝ) * (↑q : ℝ) < (2 : ℝ) ^ ((4 : ℕ) * q).
Lean, lines 135–137
```
  have hbig : (4 * q : ℝ) < 2 ^ (4 * q) := by
    have h1 : 4 * q < 2 ^ (4 * q) := Nat.lt_two_pow_self
    exact_mod_cast h1
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 135–137 at 826790afe881 ↗
1. hbig.h1 have (4 : ℕ) * q < (2 : ℕ) ^ ((4 : ℕ) * q)
  Leaves (4 : ℝ) * (↑q : ℝ) < (2 : ℝ) ^ ((4 : ℕ) * q), with h1 : (4 : ℕ) * q < (2 : ℕ) ^ ((4 : ℕ) * q).
  Uses library Nat.lt_two_pow_self.
  Lean, line 136
  have h1 : 4 * q < 2 ^ (4 * q) := Nat.lt_two_pow_self
  targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 136 at 826790afe881 ↗
h2m have (2 : ℝ) ^ m * (1 / 2 : ℝ) ^ m = (1 : ℝ)
Leaves False, with h2m : (2 : ℝ) ^ m * (1 / 2 : ℝ) ^ m = (1 : ℝ).
Uses library mul_pow.
Lean, line 138
```
  have h2m : (2 : ℝ) ^ m * (1 / 2) ^ m = 1 := by rw [← mul_pow]; norm_num
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 138 at 826790afe881 ↗
hupper have (↑q : ℝ) * (↑L : ℝ) * T < (1 : ℝ)
Leaves False, with hupper : (↑q : ℝ) * (↑L : ℝ) * T < (1 : ℝ).
Uses library mul_one.
Lean, lines 139–152
```
  have hupper : (q : ℝ) * L * T < 1 := by
    have hA1 : (q : ℝ) * L * T ≤ q * L * (4 * (1 / 2) ^ m) :=
      mul_le_mul_of_nonneg_left hTle (by positivity)
    have hA2 : (2 : ℝ) ^ (4 * q) * ((q : ℝ) * L * (4 * (1 / 2) ^ m))
        ≤ 4 * q * (2 ^ m * (1 / 2) ^ m) := by
      have := mul_le_mul_of_nonneg_right hLm' (by positivity : (0 : ℝ) ≤ 4 * q * (1 / 2) ^ m)
      nlinarith [this]
    rw [h2m, mul_one] at hA2
    have hpow : (0 : ℝ) < 2 ^ (4 * q) := by positivity
    have : (q : ℝ) * L * (4 * (1 / 2) ^ m) < 1 := by
      by_contra hc
      have hc2 := not_lt.mp hc
      nlinarith
    linarith
```
targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 139–152 at 826790afe881 ↗
1. hupper.hA1 have (↑q : ℝ) * (↑L : ℝ) * T ≤ (↑q : ℝ) * (↑L : ℝ) * ((4 : ℝ) * (1 / 2 : ℝ) ^ m)
  Leaves (↑q : ℝ) * (↑L : ℝ) * T < (1 : ℝ), with hA1 : (↑q : ℝ) * (↑L : ℝ) * T ≤ (↑q : ℝ) * (↑L : ℝ) * ((4 : ℝ) * (1 / 2 : ℝ) ^ m).
  Uses library mul_le_mul_of_nonneg_left.
  Lean, lines 140–141
  have hA1 : (q : ℝ) * L * T ≤ q * L * (4 * (1 / 2) ^ m) := mul_le_mul_of_nonneg_left hTle (by positivity)
  targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 140–141 at 826790afe881 ↗
2. hupper.hA2 have (2 : ℝ) ^ ((4 : ℕ) * q) * ((↑q : ℝ) * (↑L : ℝ) * ((4 : ℝ) * (1 / 2 : ℝ) ^ m)) ≤ (4 : ℝ) * (↑q : ℝ) * ((2 : ℝ) ^ m * (1 / 2 : ℝ) ^ m)
  Leaves (↑q : ℝ) * (↑L : ℝ) * T < (1 : ℝ), with hA2 : (2 : ℝ) ^ ((4 : ℕ) * q) * ((↑q : ℝ) * (↑L : ℝ) * ((4 : ℝ) * (1 / 2 : ℝ) ^ m)) ≤ (4 : ℝ) * (↑q : ℝ) * ((2 : ℝ) ^ m * (1 / 2 : ℝ) ^ m).
  Lean, lines 142–145
  have hA2 : (2 : ℝ) ^ (4 * q) * ((q : ℝ) * L * (4 * (1 / 2) ^ m)) ≤ 4 * q * (2 ^ m * (1 / 2) ^ m) := by have := mul_le_mul_of_nonneg_right hLm' (by positivity : (0 : ℝ) ≤ 4 * q * (1 / 2) ^ m) nlinarith [this]
  targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 142–145 at 826790afe881 ↗
  hupper.hA2.this have (2 : ℝ) ^ ((4 : ℕ) * q) * (↑L : ℝ) * ((4 : ℝ) * (↑q : ℝ) * (1 / 2 : ℝ) ^ m) ≤ (2 : ℝ) ^ m * ((4 : ℝ) * (↑q : ℝ) * (1 / 2 : ℝ) ^ m)
  Leaves (2 : ℝ) ^ ((4 : ℕ) * q) * ((↑q : ℝ) * (↑L : ℝ) * ((4 : ℝ) * (1 / 2 : ℝ) ^ m)) ≤ (4 : ℝ) * (↑q : ℝ) * ((2 : ℝ) ^ m * (1 / 2 : ℝ) ^ m), with this : (2 : ℝ) ^ ((4 : ℕ) * q) * (↑L : ℝ) * ((4 : ℝ) * (↑q : ℝ) * (1 / 2 : ℝ) ^ m) ≤ (2 : ℝ) ^ m * ((4 : ℝ) * (↑q : ℝ) * (1 / 2 : ℝ) ^ m).
  Uses library mul_le_mul_of_nonneg_right.
  Lean, line 144
  have := mul_le_mul_of_nonneg_right hLm' (by positivity : (0 : ℝ) ≤ 4 * q * (1 / 2) ^ m)
  targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 144 at 826790afe881 ↗
3. hupper.hpow have (0 : ℝ) < (2 : ℝ) ^ ((4 : ℕ) * q) routine: positivity
  Leaves (↑q : ℝ) * (↑L : ℝ) * T < (1 : ℝ), with hpow : (0 : ℝ) < (2 : ℝ) ^ ((4 : ℕ) * q).
  Lean, line 147
  have hpow : (0 : ℝ) < 2 ^ (4 * q) := by positivity
  targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 147 at 826790afe881 ↗
4. hupper.this have (↑q : ℝ) * (↑L : ℝ) * ((4 : ℝ) * (1 / 2 : ℝ) ^ m) < (1 : ℝ)
  Leaves (↑q : ℝ) * (↑L : ℝ) * T < (1 : ℝ), with this : (↑q : ℝ) * (↑L : ℝ) * ((4 : ℝ) * (1 / 2 : ℝ) ^ m) < (1 : ℝ).
  Lean, lines 148–151
  have : (q : ℝ) * L * (4 * (1 / 2) ^ m) < 1 := by by_contra hc have hc2 := not_lt.mp hc nlinarith
  targets/erdos-257/nodes/variant-1629563f/Proof.lean, lines 148–151 at 826790afe881 ↗
  hupper.this.hc2 have (1 : ℝ) ≤ (↑q : ℝ) * (↑L : ℝ) * ((4 : ℝ) * (1 / 2 : ℝ) ^ m)
  Leaves False, with hc2 : (1 : ℝ) ≤ (↑q : ℝ) * (↑L : ℝ) * ((4 : ℝ) * (1 / 2 : ℝ) ^ m).
  Uses library not_lt.
  Lean, line 150
  have hc2 := not_lt.mp hc
  targets/erdos-257/nodes/variant-1629563f/Proof.lean, line 150 at 826790afe881 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000903.json, merge commit 826790afe881.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-257/nodes/variant-1629563f/Proof.lean, sha256 554cf44ae57a.

import Mathlib
import Nodes.«variant-1629563f».Context

private lemma lac_f_nonneg (n : ℕ) : 0 ≤ (1 : ℝ) / (2 ^ n - 1) := by
  apply div_nonneg zero_le_one
  have : (1 : ℝ) ≤ 2 ^ n := one_le_pow₀ (by norm_num)
  linarith

private lemma lac_f_le (n : ℕ) : (1 : ℝ) / (2 ^ n - 1) ≤ 2 * (1 / 2) ^ n := by
  rcases Nat.eq_zero_or_pos n with rfl | hn
  · norm_num
  · have h2 : (2 : ℝ) ≤ 2 ^ n := by
      calc (2 : ℝ) = 2 ^ 1 := by norm_num
        _ ≤ 2 ^ n := pow_le_pow_right₀ (by norm_num) hn
    have hpos : (0 : ℝ) < 2 ^ n - 1 := by linarith
    have hp : (0 : ℝ) < 2 ^ n := by positivity
    rw [one_div_pow, div_le_iff₀ hpos]
    have e : (2 : ℝ) * (1 / 2 ^ n) * (2 ^ n - 1) = 2 - 2 / 2 ^ n := by
      field_simp
    have h3 : 2 / (2 : ℝ) ^ n ≤ 1 := (div_le_one hp).mpr h2
    linarith

private lemma lac_summable : Summable (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) :=
  Summable.of_nonneg_of_le lac_f_nonneg lac_f_le
    ((summable_geometric_of_lt_one (by norm_num) (by norm_num)).mul_left 2)

private lemma lac_tail_le (A : Set ℕ) (m : ℕ) :
    ∑' k : ℕ, A.indicator (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) (k + m) ≤ 4 * (1 / 2) ^ m := by
  classical
  have hrw : ∀ k : ℕ, 2 * (1 / 2 : ℝ) ^ (k + m) = (2 * (1 / 2) ^ m) * (1 / 2) ^ k := by
    intro k; rw [pow_add]; ring
  have hg : Summable (fun k : ℕ => 2 * (1 / 2 : ℝ) ^ (k + m)) := by
    simp_rw [hrw]
    exact (summable_geometric_of_lt_one (by norm_num) (by norm_num)).mul_left _
  have hle : ∀ k, A.indicator (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) (k + m)
      ≤ 2 * (1 / 2 : ℝ) ^ (k + m) := by
    intro k
    rw [Set.indicator_apply]
    split_ifs
    · exact lac_f_le _
    · positivity
  have hs : Summable (fun k : ℕ => A.indicator (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) (k + m)) :=
    Summable.of_nonneg_of_le (fun k => Set.indicator_nonneg (fun n _ => lac_f_nonneg n) _) hle hg
  calc _ ≤ ∑' k : ℕ, 2 * (1 / 2 : ℝ) ^ (k + m) := Summable.tsum_le_tsum hle hs hg
    _ = 4 * (1 / 2) ^ m := by
      simp_rw [hrw]
      rw [tsum_mul_left, tsum_geometric_of_lt_one (by norm_num) (by norm_num)]
      norm_num
      ring

private lemma liou_int (L : ℕ) (F : Finset ℕ) (hF : ∀ a ∈ F, 2 ^ a - 1 ∣ L)
    (hF0 : ∀ a ∈ F, a ≠ 0) :
    ∃ N : ℤ, (L : ℝ) * ∑ a ∈ F, (1 : ℝ) / (2 ^ a - 1) = N := by
  rw [Finset.mul_sum]
  have : ∀ a ∈ F, ∃ c : ℤ, (L : ℝ) * (1 / ((2 : ℝ) ^ a - 1)) = c := by
    intro a ha
    obtain ⟨c, hc⟩ := hF a ha
    refine ⟨c, ?_⟩
    have h1 : (1 : ℝ) < 2 ^ a := one_lt_pow₀ (by norm_num) (hF0 a ha)
    have h0 : (2 : ℝ) ^ a - 1 ≠ 0 := by linarith
    have hc' : (L : ℝ) = ((2 : ℝ) ^ a - 1) * c := by
      have h2 : 1 ≤ 2 ^ a := Nat.one_le_two_pow
      rw [hc]; push_cast [Nat.cast_sub h2]; ring
    rw [hc']; field_simp
    norm_cast
  choose c hc using this
  refine ⟨∑ a ∈ F.attach, c a.1 a.2, ?_⟩
  push_cast
  rw [← Finset.sum_attach F]
  exact Finset.sum_congr rfl (fun a _ => hc a.1 a.2)

/-- Liouville's criterion for Erdős 257: let `A` be an infinite set of positive integers such
that, for every `C`, some `m ∈ A` has a common multiple `L` of the numbers `2^a - 1` over the
elements `a < m` of `A` with `2^C · L ≤ 2^m` (the elements below `m` have a small common
denominator compared with the gap the tail leaves). Then `∑_{n ∈ A} 1/(2^n - 1)` is irrational.
Proof: if the sum were `p/q`, take `C` with `2^C > 4q`; with `L` as above, `q · L` times the tail
from `m` on is a positive integer, but the tail is below `4 · 2^(-m)`, so it is below
`4q · 2^(-C) < 1`. The criterion covers every set that is eventually lacunary of ratio two
(`Opn.erdos_257_eventually_ratio_two`: `{2^k}`, `{2^k - 1}`, `{3^k}`, `{k!}`, divisibility
chains). It does not reach sets of positive density, nor lacunary sets of ratio below two in
general; those need Erdős's arguments (1948, 1968). -/
theorem Opn.erdos_257_liouville_criterion :
    ∀ (A : Set ℕ), A.Infinite → 0 ∉ A →
    (∀ C : ℕ, ∃ m ∈ A, ∃ L : ℕ, 0 < L ∧ (∀ a ∈ A, a < m → 2 ^ a - 1 ∣ L) ∧ 2 ^ C * L ≤ 2 ^ m) →
    Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := by
  classical
  intro A _ h0 hA
  rintro ⟨r, hr⟩
  have hsum : Summable (A.indicator (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1))) :=
    lac_summable.indicator A
  have hrA : (r : ℝ) = ∑' n, A.indicator (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) n :=
    hr.trans (tsum_subtype A (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)))
  set q : ℕ := r.den with hq
  obtain ⟨m, hmA, L, hL0, hLdvd, hLm⟩ := hA (4 * q)
  have hm1 : 1 ≤ m := by
    rcases Nat.eq_zero_or_pos m with h | h
    · exact absurd (h ▸ hmA) h0
    · exact h
  set F := (Finset.range m).filter (· ∈ A) with hF
  have hsplit := hsum.sum_add_tsum_nat_add m
  have hfin : ∑ i ∈ Finset.range m, A.indicator (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) i
      = ∑ a ∈ F, (1 : ℝ) / (2 ^ a - 1) := by
    rw [hF, Finset.sum_filter]
    simp [Set.indicator_apply]
  set T := ∑' i, A.indicator (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) (i + m) with hT
  have hTs : Summable (fun i => A.indicator (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) (i + m)) :=
    (summable_nat_add_iff m).mpr hsum
  have hTpos : 0 < T := by
    apply Summable.tsum_pos hTs (fun i => Set.indicator_nonneg (fun n _ => lac_f_nonneg n) _) 0
    rw [zero_add, Set.indicator_of_mem hmA]
    have : (1 : ℝ) < 2 ^ m := one_lt_pow₀ (by norm_num) (by omega)
    apply div_pos one_pos; linarith
  have hTle : T ≤ 4 * (1 / 2) ^ m := lac_tail_le A m
  have hrT : (r : ℝ) = (∑ a ∈ F, (1 : ℝ) / (2 ^ a - 1)) + T := by
    rw [hrA, ← hsplit, hfin]
  obtain ⟨N, hN⟩ := liou_int L F
    (fun a ha => hLdvd a (Finset.mem_filter.1 ha).2 (Finset.mem_range.1 (Finset.mem_filter.1 ha).1))
    (fun a ha h => h0 (h ▸ (Finset.mem_filter.1 ha).2))
  have hPpos : (0 : ℝ) < L := by exact_mod_cast hL0
  have hqr : (r : ℝ) * q = r.num := by
    rw [hq]; exact_mod_cast Rat.mul_den_eq_num r
  have hZ : (q : ℝ) * L * T = ((L : ℤ) * r.num - q * N : ℤ) := by
    push_cast
    rw [← hN, ← hqr]
    have : T = r - ∑ a ∈ F, (1 : ℝ) / (2 ^ a - 1) := by linarith
    rw [this]; ring
  have hqpos : (0 : ℝ) < q := by
    rw [hq]; exact_mod_cast r.den_pos
  have hpos : (0 : ℝ) < (q : ℝ) * L * T := by positivity
  have hge : (1 : ℝ) ≤ (q : ℝ) * L * T := by
    rw [hZ] at hpos ⊢
    have : (0 : ℤ) < (L : ℤ) * r.num - q * N := by exact_mod_cast hpos
    exact_mod_cast this
  have hLm' : (2 : ℝ) ^ (4 * q) * L ≤ 2 ^ m := by exact_mod_cast hLm
  have hbig : (4 * q : ℝ) < 2 ^ (4 * q) := by
    have h1 : 4 * q < 2 ^ (4 * q) := Nat.lt_two_pow_self
    exact_mod_cast h1
  have h2m : (2 : ℝ) ^ m * (1 / 2) ^ m = 1 := by rw [← mul_pow]; norm_num
  have hupper : (q : ℝ) * L * T < 1 := by
    have hA1 : (q : ℝ) * L * T ≤ q * L * (4 * (1 / 2) ^ m) :=
      mul_le_mul_of_nonneg_left hTle (by positivity)
    have hA2 : (2 : ℝ) ^ (4 * q) * ((q : ℝ) * L * (4 * (1 / 2) ^ m))
        ≤ 4 * q * (2 ^ m * (1 / 2) ^ m) := by
      have := mul_le_mul_of_nonneg_right hLm' (by positivity : (0 : ℝ) ≤ 4 * q * (1 / 2) ^ m)
      nlinarith [this]
    rw [h2m, mul_one] at hA2
    have hpow : (0 : ℝ) < 2 ^ (4 * q) := by positivity
    have : (q : ℝ) * L * (4 * (1 / 2) ^ m) < 1 := by
      by_contra hc
      have hc2 := not_lt.mp hc
      nlinarith
    linarith
  linarith

What is known

Work on it

No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).

Write the explainer →

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (1 version)

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Mathlib
import Nodes.«variant-1629563f».Context

/-- Liouville's criterion for Erdős 257: let `A` be an infinite set of positive integers such
that, for every `C`, some `m ∈ A` has a common multiple `L` of the numbers `2^a - 1` over the
elements `a < m` of `A` with `2^C · L ≤ 2^m` (the elements below `m` have a small common
denominator compared with the gap the tail leaves). Then `∑_{n ∈ A} 1/(2^n - 1)` is irrational.
Proof: if the sum were `p/q`, take `C` with `2^C > 4q`; with `L` as above, `q · L` times the tail
from `m` on is a positive integer, but the tail is below `4 · 2^(-m)`, so it is below
`4q · 2^(-C) < 1`. The criterion covers every set that is eventually lacunary of ratio two
(`Opn.erdos_257_eventually_ratio_two`: `{2^k}`, `{2^k - 1}`, `{3^k}`, `{k!}`, divisibility
chains). It does not reach sets of positive density, nor lacunary sets of ratio below two in
general; those need Erdős's arguments (1948, 1968). -/
theorem Opn.erdos_257_liouville_criterion :
    ∀ (A : Set ℕ), A.Infinite → 0 ∉ A →
    (∀ C : ℕ, ∃ m ∈ A, ∃ L : ℕ, 0 < L ∧ (∀ a ∈ A, a < m → 2 ^ a - 1 ∣ L) ∧ 2 ^ C * L ≤ 2 ^ m) →
    Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := by
  sorry

In words, unverified — what this statement says; written by t1022-b, drafted with Claude Opus 5.5 via Claude Code, 2026-10-22; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

In the hypothesis $2^a - 1$ is subtraction on natural numbers, which never truncates here since $2^a \ge 1$. The sum is over the elements of $A$; $0 \notin A$ excludes Lean's junk value at $n = 0$.

The docstring's example $\{2^k - 1\}$ is to be read with $k \ge 1$: at $k = 0$ it contains $0$, which the hypothesis $0 \notin A$ excludes.

(The last paragraph is t1022-k's, from t1022-n's review; the rest is t1022-b's.)

Rendered from gloss/2d3b4c7f8488….md · Improve these words →

Rendered from targets/erdos-257/nodes/variant-1629563f/Statement.lean. Origin: variant (partial).

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000903.json, merge commit 826790afe881.

Verdict pass, from attestations/000903.json.

Submitter: t1022-b
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (intermediate)

Step	Check	Result
1	toolchain	pass
2	paths	pass
4	kernel-replay	pass
5	axioms	pass
6	hazards	pass
7	witness	pass
8	deps	pass

Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000903.json, merge commit 826790afe881.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-257/nodes/variant-1629563f/Witness.lean, sha256 bbcea2f67caf.

import Mathlib

theorem witness : ∃ (A : Set ℕ), A.Infinite ∧ (0 : ℕ) ∉ A ∧
    ∀ C : ℕ, ∃ m ∈ A, ∃ L : ℕ, 0 < L ∧ (∀ a ∈ A, a < m → 2 ^ a - 1 ∣ L) ∧ 2 ^ C * L ≤ 2 ^ m := by
  refine ⟨Set.range (fun k : ℕ => 2 ^ k),
    Set.infinite_range_of_injective (Nat.pow_right_injective (le_refl 2)), ?_, ?_⟩
  · rintro ⟨k, hk⟩
    exact absurd hk (by positivity)
  · intro C
    refine ⟨2 ^ (C + 1), ⟨C + 1, rfl⟩, 2 ^ (2 ^ C) - 1, ?_, ?_, ?_⟩
    · have : 2 ≤ 2 ^ (2 ^ C) := by
        calc 2 = 2 ^ 1 := by norm_num
          _ ≤ 2 ^ (2 ^ C) := Nat.pow_le_pow_right (by norm_num) Nat.one_le_two_pow
      omega
    · rintro a ⟨j, rfl⟩ hj
      simp only at hj ⊢
      have hjC : j ≤ C := by
        have := (Nat.pow_lt_pow_iff_right (by norm_num : 1 < 2)).1 hj
        omega
      exact Nat.pow_sub_one_dvd_pow_sub_one 2 (Nat.pow_dvd_pow 2 hjC)
    · have h1 : C ≤ 2 ^ C := Nat.lt_two_pow_self.le
      calc 2 ^ C * (2 ^ (2 ^ C) - 1) ≤ 2 ^ C * 2 ^ (2 ^ C) := Nat.mul_le_mul_left _ (Nat.sub_le _ _)
        _ = 2 ^ (C + 2 ^ C) := by rw [pow_add]
        _ ≤ 2 ^ (2 ^ (C + 1)) := Nat.pow_le_pow_right (by norm_num) (by rw [pow_succ]; omega)

No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →

Relation to the problem’s statement

Checked by the kernel — checked at admission (D-30); no proof of the node is implied.

Relation.lean — the implication between this variant and the problem’s statement, checked by the gate when the variant was admitted and immutable after (D-30). Rendered from targets/erdos-257/nodes/variant-1629563f/Relation.lean, sha256 393ebe4eb21d.

-- relation: partial
import Mathlib

/-! The variant is a partial form of the root (D-30, `partial`): the root, for every infinite
set, specialises to the sets meeting Liouville's criterion. -/

theorem relation :
    (∀ (A : Set ℕ), A.Infinite → Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1))) →
    (∀ (A : Set ℕ), A.Infinite → 0 ∉ A →
      (∀ C : ℕ, ∃ m ∈ A, ∃ L : ℕ, 0 < L ∧ (∀ a ∈ A, a < m → 2 ^ a - 1 ∣ L) ∧ 2 ^ C * L ≤ 2 ^ m) →
      Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1))) := by
  intro h A hA _ _
  exact h A hA

No gloss yet: no one has written in words what this relation says (D-3 v3.30); the Lean above is the relation. How to write one →

Acknowledged findings (2)

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at 1 / (2 ^ ↑n - 1)

Real division; the hypothesis 0 ∉ A keeps every divisor 2^n - 1 positive, so the junk value at n = 0 never enters the sum (same reading as the root's acknowledgement).

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a nat-sub finding at 2 ^ a - 1

Natural subtraction 2^a - 1 never truncates, since 2^a ≥ 1 for every a; it is the integer 2^a - 1, the denominator of the a-th term.

How to read this page

How to read a statement’s page →