Open Proof Network

Problems / erdos-69 / variant-14c6c771

Irrationality of the level sets of omega in base 2

variant-14c6c771

proved

A related variant. not yet signed as pertinent to the target (D-30 v3.12)

$\displaystyle \forall m\in\mathbb{N},\ m\ge 1:\quad \sum_{n=0}^{\infty}\bigl[\omega(n)=m\bigr]\Bigl(\frac{1}{2}\Bigr)^{n} \notin\mathbb{Q}$

For every natural m ≥ 1, the real number with a binary 1 in place n exactly when n has m distinct prime factors, the sum over n ≥ 0 of (1/2)^n when ω(n) = m and 0 otherwise, is irrational. The series is a tsum over ℝ (0 when not summable), and Irrational x means x is not the cast of a rational.

unverified · history

Lean
theorem Opn.erdos_69_omega_level_sets :
    ∀ m : ℕ, 1 ≤ m → Irrational (∑' n : ℕ, if ω n = m then (1 / 2 : ℝ) ^ n else 0) := 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, 000308, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000308.json, merge commit d69d9751de5a.

Outline of Proof.lean, extracted by the gate at 82834c4684b8 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.

  1. h_x3c9 (hω) have ∀ (n : ℕ), (ω : ℕ → ℕ) n = n.primeFactors.card

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with hω : ∀ (n : ℕ), (ω : ℕ → ℕ) n = n.primeFactors.card.

    Uses library ArithmeticFunction.cardDistinctFactors_apply, List.card_toFinset.

    Lean, lines 22–23
      have hω : ∀ n : ℕ, ω n = n.primeFactors.card := fun n => by
    rw [ArithmeticFunction.cardDistinctFactors_apply, ← List.card_toFinset]; rfl

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 22–23 at d69d9751de5a ↗

  2. Pinj have Function.Injective (Nat.nth Nat.Prime)

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with Pinj : Function.Injective (Nat.nth Nat.Prime).

    Uses library Function.Injective A function f : α → β is called injective if f x = f y implies x = y. , Nat.nth Find the n-th natural number satisfying p (indexed from 0, so nth p 0 is the first natural number satisfying p), or 0 if there is no such number. , Nat.Prime Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1. , Nat.nth_injective, Nat.infinite_setOfPred_prime A version of Nat.exists_infinite_primes using the Set.Infinite predicate. .

    Lean, line 24
      have Pinj : Function.Injective (Nat.nth Nat.Prime) := Nat.nth_injective Nat.infinite_setOfPred_prime

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 24 at d69d9751de5a ↗

  3. s3 obtain ∃ (T : ℕ → ℕ → Finset ℕ), ∀ (j c : ℕ), T j c = Finset.image (fun (i : ℕ) => Nat.nth Nat.Prime (Nat.pair j i)) (Finset.range c)

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with T : ℕ → ℕ → Finset ℕ, hT : ∀ (j c : ℕ), T j c = Finset.image (fun (i : ℕ) => Nat.nth Nat.Prime (Nat.pair j i)) (Finset.range c).

    Uses library Finset Finset α is the type of finite sets of elements of α. , Finset.range range n is the set of natural numbers less than n. , Nat.nth Find the n-th natural number satisfying p (indexed from 0, so nth p 0 is the first natural number satisfying p), or 0 if there is no such number. , Nat.Prime Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1. , Nat.pair Pairing function for the natural numbers. , Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, lines 26–28
      obtain ⟨T, hT⟩ : ∃ T : ℕ → ℕ → Finset ℕ, ∀ j c,
      T j c = (Finset.range c).image (fun i => Nat.nth Nat.Prime (Nat.pair j i)) :=
    ⟨fun j c => _, fun _ _ => rfl⟩

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 26–28 at d69d9751de5a ↗

  4. T_prime have ∀ (j c p : ℕ), p ∈ T j c → Nat.Prime p

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with T_prime : ∀ (j c p : ℕ), p ∈ T j c → Nat.Prime p.

    Uses library Nat.prime_nth_prime.

    Lean, lines 29–33
      have T_prime : ∀ j c, ∀ p ∈ T j c, p.Prime := by
    intro j c p hp
    rw [hT] at hp
    obtain ⟨i, -, rfl⟩ := Finset.mem_image.mp hp
    exact Nat.prime_nth_prime _

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 29–33 at d69d9751de5a ↗

    1. T_prime.s1 obtain ∃ a ∈ Finset.range c, Nat.nth Nat.Prime (Nat.pair j a) = p

      Leaves Nat.Prime (Nat.nth Nat.Prime (Nat.pair j i)), with i : ℕ, hp : Nat.nth Nat.Prime (Nat.pair j i) ∈ Finset.image (fun (i : ℕ) => Nat.nth Nat.Prime (Nat.pair j i)) (Finset.range c).

      Uses library Finset.mem_image.

      Lean, line 32
          obtain ⟨i, -, rfl⟩ := Finset.mem_image.mp hp

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 32 at d69d9751de5a ↗

  5. T_card have ∀ (j c : ℕ), (T j c).card = c

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with T_card : ∀ (j c : ℕ), (T j c).card = c.

    Uses library Finset.card_image_of_injective, Nat.pair_eq_pair, Finset.card_range.

    Lean, lines 34–37
      have T_card : ∀ j c, (T j c).card = c := by
    intro j c
    rw [hT, Finset.card_image_of_injective _ (fun a b h => (Nat.pair_eq_pair.mp (Pinj h)).2),
      Finset.card_range]

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 34–37 at d69d9751de5a ↗

  6. T_disj have ∀ (j j' c c' : ℕ), j ≠ j' → ∀ p ∈ T j c, ∀ q ∈ T j' c', p ≠ q

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with T_disj : ∀ (j j' c c' : ℕ), j ≠ j' → ∀ p ∈ T j c, ∀ q ∈ T j' c', p ≠ q.

    Uses library Nat.pair_eq_pair.

    Lean, lines 38–43
      have T_disj : ∀ j j' c c', j ≠ j' → ∀ p ∈ T j c, ∀ q ∈ T j' c', p ≠ q := by
    intro j j' c c' hjj p hp q hq hpq
    rw [hT] at hp hq
    obtain ⟨i, -, rfl⟩ := Finset.mem_image.mp hp
    obtain ⟨i', -, rfl⟩ := Finset.mem_image.mp hq
    exact hjj (Nat.pair_eq_pair.mp (Pinj hpq)).1

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 38–43 at d69d9751de5a ↗

    1. T_disj.s1 obtain ∃ a ∈ Finset.range c, Nat.nth Nat.Prime (Nat.pair j a) = p

      Leaves False, with i : ℕ, hp : Nat.nth Nat.Prime (Nat.pair j i) ∈ Finset.image (fun (i : ℕ) => Nat.nth Nat.Prime (Nat.pair j i)) (Finset.range c), hpq : Nat.nth Nat.Prime (Nat.pair j i) = q.

      Uses library Finset.mem_image.

      Lean, line 41
          obtain ⟨i, -, rfl⟩ := Finset.mem_image.mp hp

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 41 at d69d9751de5a ↗

    2. T_disj.s2 obtain ∃ a ∈ Finset.range c', Nat.nth Nat.Prime (Nat.pair j' a) = q

      Leaves False, with i' : ℕ, hq : Nat.nth Nat.Prime (Nat.pair j' i') ∈ Finset.image (fun (i : ℕ) => Nat.nth Nat.Prime (Nat.pair j' i)) (Finset.range c'), hpq : Nat.nth Nat.Prime (Nat.pair j i) = Nat.nth Nat.Prime (Nat.pair j' i').

      Uses library Finset.mem_image.

      Lean, line 42
          obtain ⟨i', -, rfl⟩ := Finset.mem_image.mp hq

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 42 at d69d9751de5a ↗

  7. prod_pf have ∀ (j c : ℕ), (∏ p ∈ T j c, p).primeFactors = T j c

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with prod_pf : ∀ (j c : ℕ), (∏ p ∈ T j c, p).primeFactors = T j c.

    Uses library Nat.primeFactors_prod.

    Lean, lines 44–45
      have prod_pf : ∀ j c, (∏ p ∈ T j c, p).primeFactors = T j c :=
    fun j c => Nat.primeFactors_prod (T_prime j c)

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 44–45 at d69d9751de5a ↗

  8. s8 obtain ∃ (Q : ℕ → ℕ), ∀ (j : ℕ), Q j = ∏ p ∈ T j (m + (1 : ℕ)), p

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with Q : ℕ → ℕ, hQ : ∀ (j : ℕ), Q j = ∏ p ∈ T j (m + (1 : ℕ)), p.

    Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, line 47
      obtain ⟨Q, hQ⟩ : ∃ Q : ℕ → ℕ, ∀ j, Q j = ∏ p ∈ T j (m + 1), p := ⟨fun j => _, fun _ => rfl⟩

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 47 at d69d9751de5a ↗

  9. Qpos have ∀ (j : ℕ), (0 : ℕ) < Q j

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with Qpos : ∀ (j : ℕ), (0 : ℕ) < Q j.

    Uses library Finset.prod_pos.

    Lean, lines 48–49
      have Qpos : ∀ j, 0 < Q j := fun j => by
    rw [hQ]; exact Finset.prod_pos (fun p hp => (T_prime j (m + 1) p hp).pos)

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 48–49 at d69d9751de5a ↗

  10. Qcop have ∀ (j j' : ℕ), j ≠ j' → (Q j).Coprime (Q j')

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with Qcop : ∀ (j j' : ℕ), j ≠ j' → (Q j).Coprime (Q j').

    Uses library Nat.Coprime m and n are coprime, or relatively prime, if their gcd is 1. , Nat.Coprime.prod_left See IsCoprime.prod_left for the corresponding lemma about IsCoprime , Nat.Coprime.prod_right See IsCoprime.prod_right for the corresponding lemma about IsCoprime , Nat.coprime_primes.

    Lean, lines 50–58
      have Qcop : ∀ j j', j ≠ j' → Nat.Coprime (Q j) (Q j') := by
    intro j j' hjj
    rw [hQ j, hQ j']
    apply Nat.Coprime.prod_left
    intro p hp
    apply Nat.Coprime.prod_right
    intro q hq
    exact (Nat.coprime_primes (T_prime _ _ p hp) (T_prime _ _ q hq)).mpr
      (T_disj j j' _ _ hjj p hp q hq)

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 50–58 at d69d9751de5a ↗

  11. window have ∀ (k : ℕ), ∃ (N : ℕ), ∀ j < k, (ω : ℕ → ℕ) (j + (N + (1 : ℕ))) ≠ m

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with window : ∀ (k : ℕ), ∃ (N : ℕ), ∀ j < k, (ω : ℕ → ℕ) (j + (N + (1 : ℕ))) ≠ m.

    Uses library Exists.intro Existential introduction. .

    Lean, lines 60–78
      have window : ∀ k : ℕ, ∃ N : ℕ, ∀ j, j < k → ω (j + (N + 1)) ≠ m := by
    intro k
    obtain ⟨N, hN⟩ := Nat.chineseRemainderOfFinset (fun j => Q j - (j + 1) % Q j) Q
      (Finset.range k) (fun j _ => (Qpos j).ne') (fun j _ j' _ hjj => Qcop j j' hjj)
    refine ⟨N, fun j hj => ?_⟩
    have hmod := hN j (Finset.mem_range.mpr hj)
    have hdvd : Q j ∣ j + (N + 1) := by
      have h1 : N + (j + 1) ≡ (Q j - (j + 1) % Q j) + (j + 1) % Q j [MOD Q j] :=
        Nat.ModEq.add hmod (Nat.mod_modEq (j + 1) (Q j)).symm
      rw [Nat.sub_add_cancel (Nat.mod_lt _ (Qpos j)).le] at h1
      have h2 : N + (j + 1) ≡ 0 [MOD Q j] := h1.trans (Nat.modEq_zero_iff_dvd.mpr dvd_rfl)
      have h3 := Nat.modEq_zero_iff_dvd.mp h2
      rwa [show j + (N + 1) = N + (j + 1) by ring]
    have hsub : T j (m + 1) ⊆ (j + (N + 1)).primeFactors := by
      rw [← prod_pf j (m + 1), ← hQ]
      exact Nat.primeFactors_mono hdvd (by omega)
    have hcard := Finset.card_le_card hsub
    rw [T_card] at hcard
    rw [hω]; omega

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 60–78 at d69d9751de5a ↗

    1. window.s1 obtain { k_1 : ℕ // ∀ i ∈ Finset.range k, k_1 ≡ Q i - (i + (1 : ℕ)) % Q i [MOD Q i] }

      Leaves ∃ (N : ℕ), ∀ j < k, (ω : ℕ → ℕ) (j + (N + (1 : ℕ))) ≠ m, with N : ℕ, hN : ∀ i ∈ Finset.range k, N ≡ Q i - (i + (1 : ℕ)) % Q i [MOD Q i].

      Uses library Nat.chineseRemainderOfFinset The natural number less than ∏ i ∈ t, s i congruent to a i mod s i for all i ∈ t. , Finset.range range n is the set of natural numbers less than n. .

      Lean, lines 62–63
          obtain ⟨N, hN⟩ := Nat.chineseRemainderOfFinset (fun j => Q j - (j + 1) % Q j) Q
      (Finset.range k) (fun j _ => (Qpos j).ne') (fun j _ j' _ hjj => Qcop j j' hjj)

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 62–63 at d69d9751de5a ↗

    2. window.hmod have N ≡ Q j - (j + (1 : ℕ)) % Q j [MOD Q j]

      Leaves (ω : ℕ → ℕ) (j + (N + (1 : ℕ))) ≠ m, with hmod : N ≡ Q j - (j + (1 : ℕ)) % Q j [MOD Q j].

      Uses library Finset.mem_range.

      Lean, line 65
          have hmod := hN j (Finset.mem_range.mpr hj)

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 65 at d69d9751de5a ↗

    3. window.hdvd have Q j ∣ j + (N + (1 : ℕ))

      Leaves (ω : ℕ → ℕ) (j + (N + (1 : ℕ))) ≠ m, with hdvd : Q j ∣ j + (N + (1 : ℕ)).

      Uses library Nat.sub_add_cancel, Nat.mod_lt.

      Lean, lines 66–72
          have hdvd : Q j ∣ j + (N + 1) := by
      have h1 : N + (j + 1) ≡ (Q j - (j + 1) % Q j) + (j + 1) % Q j [MOD Q j] :=
        Nat.ModEq.add hmod (Nat.mod_modEq (j + 1) (Q j)).symm
      rw [Nat.sub_add_cancel (Nat.mod_lt _ (Qpos j)).le] at h1
      have h2 : N + (j + 1) ≡ 0 [MOD Q j] := h1.trans (Nat.modEq_zero_iff_dvd.mpr dvd_rfl)
      have h3 := Nat.modEq_zero_iff_dvd.mp h2
      rwa [show j + (N + 1) = N + (j + 1) by ring]

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 66–72 at d69d9751de5a ↗

      1. window.hdvd.h1 have N + (j + (1 : ℕ)) ≡ Q j - (j + (1 : ℕ)) % Q j + (j + (1 : ℕ)) % Q j [MOD Q j]

        Leaves Q j ∣ j + (N + (1 : ℕ)), with h1 : N + (j + (1 : ℕ)) ≡ Q j - (j + (1 : ℕ)) % Q j + (j + (1 : ℕ)) % Q j [MOD Q j].

        Uses library Nat.ModEq.add, Nat.mod_modEq.

        Lean, lines 67–68
              have h1 : N + (j + 1) ≡ (Q j - (j + 1) % Q j) + (j + 1) % Q j [MOD Q j] :=
        Nat.ModEq.add hmod (Nat.mod_modEq (j + 1) (Q j)).symm

        targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 67–68 at d69d9751de5a ↗

      2. window.hdvd.h2 have N + (j + (1 : ℕ)) ≡ (0 : ℕ) [MOD Q j]

        Leaves Q j ∣ j + (N + (1 : ℕ)), with h2 : N + (j + (1 : ℕ)) ≡ (0 : ℕ) [MOD Q j].

        Uses library Nat.modEq_zero_iff_dvd, dvd_rfl.

        Lean, line 70
              have h2 : N + (j + 1) ≡ 0 [MOD Q j] := h1.trans (Nat.modEq_zero_iff_dvd.mpr dvd_rfl)

        targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 70 at d69d9751de5a ↗

      3. window.hdvd.h3 have Q j ∣ N + (j + (1 : ℕ))

        Leaves Q j ∣ j + (N + (1 : ℕ)), with h3 : Q j ∣ N + (j + (1 : ℕ)).

        Uses library Nat.modEq_zero_iff_dvd.

        Lean, line 71
              have h3 := Nat.modEq_zero_iff_dvd.mp h2

        targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 71 at d69d9751de5a ↗

    4. window.hsub have T j (m + (1 : ℕ)) ⊆ (j + (N + (1 : ℕ))).primeFactors

      Leaves (ω : ℕ → ℕ) (j + (N + (1 : ℕ))) ≠ m, with hsub : T j (m + (1 : ℕ)) ⊆ (j + (N + (1 : ℕ))).primeFactors.

      Uses library Nat.primeFactors_mono.

      Lean, lines 73–75
          have hsub : T j (m + 1) ⊆ (j + (N + 1)).primeFactors := by
      rw [← prod_pf j (m + 1), ← hQ]
      exact Nat.primeFactors_mono hdvd (by omega)

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 73–75 at d69d9751de5a ↗

    5. window.hcard have (T j (m + (1 : ℕ))).card ≤ (j + (N + (1 : ℕ))).primeFactors.card

      Leaves (ω : ℕ → ℕ) (j + (N + (1 : ℕ))) ≠ m, with hcard : (T j (m + (1 : ℕ))).card ≤ (j + (N + (1 : ℕ))).primeFactors.card.

      Uses library Finset.card_le_card.

      Lean, line 76
          have hcard := Finset.card_le_card hsub

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 76 at d69d9751de5a ↗

  12. s12 obtain ∃ (W : ℕ), W = ∏ p ∈ T (0 : ℕ) m, p

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with W : ℕ, hW : W = ∏ p ∈ T (0 : ℕ) m, p.

    Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, line 80
      obtain ⟨W, hW⟩ : ∃ W : ℕ, W = ∏ p ∈ T 0 m, p := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 80 at d69d9751de5a ↗

  13. Wc have W.primeFactors.card = m

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with Wc : W.primeFactors.card = m.

    Lean, line 81
      have Wc : W.primeFactors.card = m := by rw [hW, prod_pf, T_card]

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 81 at d69d9751de5a ↗

  14. W2 have (2 : ℕ) ≤ W

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with W2 : (2 : ℕ) ≤ W.

    Uses library Nat.lt_or_ge.

    Lean, lines 82–85
      have W2 : 2 ≤ W := by
    rcases Nat.lt_or_ge W 2 with h | h
    · interval_cases W <;> simp at Wc <;> omega
    · exact h

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 82–85 at d69d9751de5a ↗

    1. W2.s1 case

      Leaves (2 : ℕ) ≤ W.

      Lean, line 84
          · interval_cases W <;> simp at Wc <;> omega

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 84 at d69d9751de5a ↗

    2. W2.s2 case

      Leaves (2 : ℕ) ≤ W.

      Lean, line 85
          · exact h

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 85 at d69d9751de5a ↗

  15. many have ∀ (L : ℕ), ∃ (n : ℕ), L ≤ n ∧ (ω : ℕ → ℕ) n = m

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with many : ∀ (L : ℕ), ∃ (n : ℕ), L ≤ n ∧ (ω : ℕ → ℕ) n = m.

    Uses library Exists.intro Existential introduction. .

    Lean, lines 86–92
      have many : ∀ L : ℕ, ∃ n, L ≤ n ∧ ω n = m := by
    intro L
    refine ⟨W ^ (L + 1), ?_, ?_⟩
    · calc L ≤ 2 ^ L := Nat.lt_two_pow_self.le
        _ ≤ 2 ^ (L + 1) := Nat.pow_le_pow_right (by norm_num) (by omega)
        _ ≤ W ^ (L + 1) := Nat.pow_le_pow_left W2 _
    · rw [hω, Nat.primeFactors_pow _ (by omega), Wc]

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 86–92 at d69d9751de5a ↗

    1. many.s1 case

      Leaves L ≤ W ^ (L + (1 : ℕ)).

      Lean, lines 89–91
          · calc L ≤ 2 ^ L := Nat.lt_two_pow_self.le
        _ ≤ 2 ^ (L + 1) := Nat.pow_le_pow_right (by norm_num) (by omega)
        _ ≤ W ^ (L + 1) := Nat.pow_le_pow_left W2 _

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 89–91 at d69d9751de5a ↗

      1. many.s1.s1 calc L ≤ (2 : ℕ) ^ L

        Closes the goal.

        Uses library Nat.lt_two_pow_self.

        Lean, line 89
            · calc L ≤ 2 ^ L := Nat.lt_two_pow_self.le

        targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 89 at d69d9751de5a ↗

      2. many.s1.s2 calc (2 : ℕ) ^ L ≤ (2 : ℕ) ^ (L + (1 : ℕ))

        Closes the goal.

        Uses library Nat.pow_le_pow_right.

        Lean, line 90
                _ ≤ 2 ^ (L + 1) := Nat.pow_le_pow_right (by norm_num) (by omega)

        targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 90 at d69d9751de5a ↗

      3. many.s1.s3 calc (2 : ℕ) ^ (L + (1 : ℕ)) ≤ W ^ (L + (1 : ℕ))

        Closes the goal.

        Uses library Nat.pow_le_pow_left.

        Lean, line 91
                _ ≤ W ^ (L + 1) := Nat.pow_le_pow_left W2 _

        targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 91 at d69d9751de5a ↗

    2. many.s2 case

      Leaves (ω : ℕ → ℕ) (W ^ (L + (1 : ℕ))) = m.

      Uses library Nat.primeFactors_pow.

      Lean, line 92
          · rw [hω, Nat.primeFactors_pow _ (by omega), Wc]

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 92 at d69d9751de5a ↗

  16. s16 obtain ∃ (b : ℕ), b = (2 : ℕ)

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with b : ℕ, hbdef : b = (2 : ℕ).

    Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, line 93
      obtain ⟨b, hbdef⟩ : ∃ b : ℕ, b = 2 := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 93 at d69d9751de5a ↗

  17. hb have (2 : ℕ) ≤ b routine: omega

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with hb : (2 : ℕ) ≤ b.

    Lean, line 94
      have hb : 2 ≤ b := by omega

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 94 at d69d9751de5a ↗

  18. hb0 have (2 : ℝ) ≤ (↑b : ℝ)

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with hb0 : (2 : ℝ) ≤ (↑b : ℝ).

    Lean, line 95
      have hb0 : (2 : ℝ) ≤ (b : ℝ) := by exact_mod_cast hb

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 95 at d69d9751de5a ↗

  19. bpos have (0 : ℝ) < (↑b : ℝ) routine: linarith

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with bpos : (0 : ℝ) < (↑b : ℝ).

    Lean, line 96
      have bpos : (0 : ℝ) < b := by linarith

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 96 at d69d9751de5a ↗

  20. s20 obtain ∃ (r : ℝ), r = (1 : ℝ) / (↑b : ℝ)

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with r : ℝ, hr : r = (1 : ℝ) / (↑b : ℝ).

    Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, line 97
      obtain ⟨r, hr⟩ : ∃ r : ℝ, r = 1 / (b : ℝ) := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 97 at d69d9751de5a ↗

  21. r0 have (0 : ℝ) < r

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with r0 : (0 : ℝ) < r.

    Uses library one_div_pos.

    Lean, line 98
      have r0 : 0 < r := by rw [hr]; exact one_div_pos.mpr bpos

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 98 at d69d9751de5a ↗

  22. r2 have r ≤ (1 / 2 : ℝ)

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with r2 : r ≤ (1 / 2 : ℝ).

    Uses library one_div_le_one_div_of_le.

    Lean, line 99
      have r2 : r ≤ 1 / 2 := by rw [hr]; exact one_div_le_one_div_of_le (by norm_num) hb0

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 99 at d69d9751de5a ↗

  23. rb have r * (↑b : ℝ) = (1 : ℝ)

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with rb : r * (↑b : ℝ) = (1 : ℝ).

    Uses library one_div, inv_mul_cancel₀.

    Lean, line 100
      have rb : r * (b : ℝ) = 1 := by rw [hr, one_div, inv_mul_cancel₀ bpos.ne']

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 100 at d69d9751de5a ↗

  24. r12 have r = (1 / 2 : ℝ)

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with r12 : r = (1 / 2 : ℝ).

    Lean, line 101
      have r12 : r = 1 / 2 := by rw [hr, hbdef]; norm_num

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 101 at d69d9751de5a ↗

  25. s25 obtain ∃ (f : ℕ → ℝ), f = fun (n : ℕ) => if (ω : ℕ → ℕ) n = m then r ^ n else (0 : ℝ)

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with f : ℕ → ℝ, hf : f = fun (n : ℕ) => if (ω : ℕ → ℕ) n = m then r ^ n else (0 : ℝ).

    Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, line 102
      obtain ⟨f, hf⟩ : ∃ f : ℕ → ℝ, f = fun n => if ω n = m then r ^ n else 0 := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 102 at d69d9751de5a ↗

  26. hconv have (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)) = ∑' (n : ℕ), f n routine: simp

    Leaves Irrational (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)), with hconv : (∑' (n : ℕ), if (ω : ℕ → ℕ) n = m then (1 / 2 : ℝ) ^ n else (0 : ℝ)) = ∑' (n : ℕ), f n.

    Lean, lines 103–104
      have hconv : (∑' n : ℕ, if ω n = m then (1 / 2 : ℝ) ^ n else 0) = ∑' n : ℕ, f n := by
    simp only [hf, r12]

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 103–104 at d69d9751de5a ↗

  27. f_nonneg have ∀ (n : ℕ), (0 : ℝ) ≤ f n

    Leaves Irrational (∑' (n : ℕ), f n), with f_nonneg : ∀ (n : ℕ), (0 : ℝ) ≤ f n.

    Lean, lines 106–109
      have f_nonneg : ∀ n, 0 ≤ f n := fun n => by
    simp only [hf]; split_ifs
    · exact pow_nonneg r0.le n
    · exact le_rfl

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 106–109 at d69d9751de5a ↗

    1. f_nonneg.s1 case

      Leaves (0 : ℝ) ≤ r ^ n.

      Uses library pow_nonneg.

      Lean, line 108
          · exact pow_nonneg r0.le n

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 108 at d69d9751de5a ↗

    2. f_nonneg.s2 case

      Leaves (0 : ℝ) ≤ (0 : ℝ).

      Uses library le_rfl A version of le_refl where the argument is implicit .

      Lean, line 109
          · exact le_rfl

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 109 at d69d9751de5a ↗

  28. f_le have ∀ (n : ℕ), f n ≤ r ^ n

    Leaves Irrational (∑' (n : ℕ), f n), with f_le : ∀ (n : ℕ), f n ≤ r ^ n.

    Lean, lines 110–113
      have f_le : ∀ n, f n ≤ r ^ n := fun n => by
    simp only [hf]; split_ifs
    · exact le_rfl
    · exact pow_nonneg r0.le n

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 110–113 at d69d9751de5a ↗

    1. f_le.s1 case

      Leaves r ^ n ≤ r ^ n.

      Uses library le_rfl A version of le_refl where the argument is implicit .

      Lean, line 112
          · exact le_rfl

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 112 at d69d9751de5a ↗

    2. f_le.s2 case

      Leaves (0 : ℝ) ≤ r ^ n.

      Uses library pow_nonneg.

      Lean, line 113
          · exact pow_nonneg r0.le n

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 113 at d69d9751de5a ↗

  29. hs have Summable f

    Leaves Irrational (∑' (n : ℕ), f n), with hs : Summable f.

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , Summable.of_nonneg_of_le Comparison test of convergence of series of non-negative real numbers. , summable_geometric_of_lt_one.

    Lean, lines 114–116
      have hs : Summable f :=
    Summable.of_nonneg_of_le f_nonneg f_le
      (summable_geometric_of_lt_one r0.le (by linarith))

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 114–116 at d69d9751de5a ↗

  30. s30 obtain ∃ (k : ℕ), k = q.den

    Leaves False, with k : ℕ, hk : k = q.den.

    Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, line 118
      obtain ⟨k, hk⟩ : ∃ k, k = q.den := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 118 at d69d9751de5a ↗

  31. kpos have (0 : ℕ) < k

    Leaves False, with kpos : (0 : ℕ) < k.

    Lean, line 119
      have kpos : 0 < k := by rw [hk]; exact q.den_pos

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 119 at d69d9751de5a ↗

  32. s32 obtain ∃ (N : ℕ), ∀ j < k, (ω : ℕ → ℕ) (j + (N + (1 : ℕ))) ≠ m

    Leaves False, with N : ℕ, hNw : ∀ j < k, (ω : ℕ → ℕ) (j + (N + (1 : ℕ))) ≠ m.

    Lean, line 120
      obtain ⟨N, hNw⟩ := window k

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 120 at d69d9751de5a ↗

  33. comp have ∀ j < k, f (j + (N + (1 : ℕ))) = (0 : ℝ)

    Leaves False, with comp : ∀ j < k, f (j + (N + (1 : ℕ))) = (0 : ℝ).

    Uses library if_neg.

    Lean, lines 121–124
      have comp : ∀ j, j < k → f (j + (N + 1)) = 0 := by
    intro j hj
    simp only [hf]
    rw [if_neg (hNw j hj)]

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 121–124 at d69d9751de5a ↗

  34. hg have Summable fun (i : ℕ) => f (i + (N + (1 : ℕ)))

    Leaves False, with hg : Summable fun (i : ℕ) => f (i + (N + (1 : ℕ))).

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , summable_nat_add_iff.

    Lean, line 125
      have hg : Summable (fun i => f (i + (N + 1))) := (summable_nat_add_iff (N + 1)).mpr hs

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 125 at d69d9751de5a ↗

  35. hg' have Summable fun (i : ℕ) => f (i + k + (N + (1 : ℕ)))

    Leaves False, with hg' : Summable fun (i : ℕ) => f (i + k + (N + (1 : ℕ))).

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , add_assoc.

    Lean, lines 126–128
      have hg' : Summable (fun i => f (i + k + (N + 1))) := by
    have := (summable_nat_add_iff k).mpr hg
    simpa [add_assoc] using this

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 126–128 at d69d9751de5a ↗

    1. hg'.this have Summable fun (n : ℕ) => f (n + k + (N + (1 : ℕ)))

      Leaves Summable fun (i : ℕ) => f (i + k + (N + (1 : ℕ))), with this : Summable fun (n : ℕ) => f (n + k + (N + (1 : ℕ))).

      Uses library summable_nat_add_iff.

      Lean, line 127
          have := (summable_nat_add_iff k).mpr hg

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 127 at d69d9751de5a ↗

  36. split1 have ∑ i ∈ Finset.range (N + (1 : ℕ)), f i + ∑' (i : ℕ), f (i + (N + (1 : ℕ))) = ∑' (i : ℕ), f i

    Leaves False, with split1 : ∑ i ∈ Finset.range (N + (1 : ℕ)), f i + ∑' (i : ℕ), f (i + (N + (1 : ℕ))) = ∑' (i : ℕ), f i.

    Uses library Summable.sum_add_tsum_nat_add.

    Lean, line 129
      have split1 := Summable.sum_add_tsum_nat_add (N + 1) hs

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 129 at d69d9751de5a ↗

  37. split2 have ∑ i ∈ Finset.range k, f (i + (N + (1 : ℕ))) + ∑' (i : ℕ), f (i + k + (N + (1 : ℕ))) = ∑' (i : ℕ), f (i + (N + (1 : ℕ)))

    Leaves False, with split2 : ∑ i ∈ Finset.range k, f (i + (N + (1 : ℕ))) + ∑' (i : ℕ), f (i + k + (N + (1 : ℕ))) = ∑' (i : ℕ), f (i + (N + (1 : ℕ))).

    Uses library Summable.sum_add_tsum_nat_add.

    Lean, line 130
      have split2 := Summable.sum_add_tsum_nat_add k hg

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 130 at d69d9751de5a ↗

  38. zero_part have ∑ i ∈ Finset.range k, f (i + (N + (1 : ℕ))) = (0 : ℝ)

    Leaves False, with zero_part : ∑ i ∈ Finset.range k, f (i + (N + (1 : ℕ))) = (0 : ℝ).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.sum_eq_zero, Finset.mem_range.

    Lean, lines 131–134
      have zero_part : ∑ i ∈ Finset.range k, f (i + (N + 1)) = 0 := by
    apply Finset.sum_eq_zero
    intro j hj
    exact comp j (Finset.mem_range.mp hj)

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 131–134 at d69d9751de5a ↗

  39. s39 obtain ∃ (R : ℝ), R = ∑' (i : ℕ), f (i + k + (N + (1 : ℕ)))

    Leaves False, with R : ℝ, hR : R = ∑' (i : ℕ), f (i + k + (N + (1 : ℕ))).

    Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, line 135
      obtain ⟨R, hR⟩ : ∃ R, R = ∑' i, f (i + k + (N + 1)) := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 135 at d69d9751de5a ↗

  40. split2' have ∑' (i : ℕ), f (i + (N + (1 : ℕ))) = R

    Leaves False, with split2' : ∑' (i : ℕ), f (i + (N + (1 : ℕ))) = R.

    Uses library zero_add.

    Lean, lines 136–137
      have split2' : ∑' i, f (i + (N + 1)) = R := by
    rw [← split2, zero_part, zero_add, hR]

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 136–137 at d69d9751de5a ↗

  41. Rpos have (0 : ℝ) < R

    Leaves False, with Rpos : (0 : ℝ) < R.

    Uses library if_pos, pow_pos.

    Lean, lines 138–144
      have Rpos : 0 < R := by
    obtain ⟨p, hp1, hp2⟩ := many (k + (N + 1))
    have hpi : p - (k + (N + 1)) + k + (N + 1) = p := by omega
    rw [hR]
    refine hg'.tsum_pos (fun i => f_nonneg _) (p - (k + (N + 1))) ?_
    rw [hpi]; simp only [hf, if_pos hp2]
    exact pow_pos r0 p

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 138–144 at d69d9751de5a ↗

    1. Rpos.s1 obtain ∃ (n : ℕ), k + (N + (1 : ℕ)) ≤ n ∧ (ω : ℕ → ℕ) n = m

      Leaves (0 : ℝ) < R, with p : ℕ, hp1 : k + (N + (1 : ℕ)) ≤ p, hp2 : (ω : ℕ → ℕ) p = m.

      Lean, line 139
          obtain ⟨p, hp1, hp2⟩ := many (k + (N + 1))

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 139 at d69d9751de5a ↗

    2. Rpos.hpi have p - (k + (N + (1 : ℕ))) + k + (N + (1 : ℕ)) = p routine: omega

      Leaves (0 : ℝ) < R, with hpi : p - (k + (N + (1 : ℕ))) + k + (N + (1 : ℕ)) = p.

      Lean, line 140
          have hpi : p - (k + (N + 1)) + k + (N + 1) = p := by omega

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 140 at d69d9751de5a ↗

  42. geo have Summable fun (i : ℕ) => r ^ (k + (N + (1 : ℕ))) * (1 / 2 : ℝ) ^ i

    Leaves False, with geo : Summable fun (i : ℕ) => r ^ (k + (N + (1 : ℕ))) * (1 / 2 : ℝ) ^ i.

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , summable_geometric_two.

    Lean, lines 145–146
      have geo : Summable (fun i : ℕ => r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i) :=
    summable_geometric_two.mul_left _

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 145–146 at d69d9751de5a ↗

  43. term_le have ∀ (i : ℕ), f (i + k + (N + (1 : ℕ))) ≤ r ^ (k + (N + (1 : ℕ))) * (1 / 2 : ℝ) ^ i

    Leaves False, with term_le : ∀ (i : ℕ), f (i + k + (N + (1 : ℕ))) ≤ r ^ (k + (N + (1 : ℕ))) * (1 / 2 : ℝ) ^ i.

    Lean, lines 147–152
      have term_le : ∀ i, f (i + k + (N + 1)) ≤ r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i := by
    intro i
    calc f (i + k + (N + 1)) ≤ r ^ (i + k + (N + 1)) := f_le _
      _ = r ^ (k + (N + 1)) * r ^ i := by ring
      _ ≤ r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i :=
        mul_le_mul_of_nonneg_left (pow_le_pow_left₀ r0.le r2 i) (pow_nonneg r0.le _)

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 147–152 at d69d9751de5a ↗

    1. term_le.s1 calc f (i + k + (N + (1 : ℕ))) ≤ r ^ (i + k + (N + (1 : ℕ)))

      Closes the goal.

      Lean, line 149
          calc f (i + k + (N + 1)) ≤ r ^ (i + k + (N + 1)) := f_le _

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 149 at d69d9751de5a ↗

    2. term_le.s2 calc routine: ring

      Closes the goal.

      Lean, line 150
            _ = r ^ (k + (N + 1)) * r ^ i := by ring

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 150 at d69d9751de5a ↗

    3. term_le.s3 calc r ^ (k + (N + (1 : ℕ))) * r ^ i ≤ r ^ (k + (N + (1 : ℕ))) * (1 / 2 : ℝ) ^ i

      Closes the goal.

      Uses library mul_le_mul_of_nonneg_left, pow_le_pow_left₀, pow_nonneg.

      Lean, lines 151–152
            _ ≤ r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i :=
        mul_le_mul_of_nonneg_left (pow_le_pow_left₀ r0.le r2 i) (pow_nonneg r0.le _)

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 151–152 at d69d9751de5a ↗

  44. Rle have R ≤ r ^ (k + (N + (1 : ℕ))) * (2 : ℝ)

    Leaves False, with Rle : R ≤ r ^ (k + (N + (1 : ℕ))) * (2 : ℝ).

    Lean, lines 153–157
      have Rle : R ≤ r ^ (k + (N + 1)) * 2 := by
    rw [hR]
    calc ∑' i, f (i + k + (N + 1)) ≤ ∑' i : ℕ, r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i :=
          Summable.tsum_le_tsum term_le hg' geo
      _ = r ^ (k + (N + 1)) * 2 := by rw [tsum_mul_left, tsum_geometric_two]

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 153–157 at d69d9751de5a ↗

    1. Rle.s1 calc ∑' (i : ℕ), f (i + k + (N + (1 : ℕ))) ≤ ∑' (i : ℕ), r ^ (k + (N + (1 : ℕ))) * (1 / 2 : ℝ) ^ i

      Closes the goal.

      Uses library Summable.tsum_le_tsum.

      Lean, lines 155–156
          calc ∑' i, f (i + k + (N + 1)) ≤ ∑' i : ℕ, r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i :=
          Summable.tsum_le_tsum term_le hg' geo

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 155–156 at d69d9751de5a ↗

    2. Rle.s2 calc

      Closes the goal.

      Uses library tsum_mul_left, tsum_geometric_two.

      Lean, line 157
            _ = r ^ (k + (N + 1)) * 2 := by rw [tsum_mul_left, tsum_geometric_two]

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 157 at d69d9751de5a ↗

  45. bN have (↑b : ℝ) ^ N * r ^ N = (1 : ℝ)

    Leaves False, with bN : (↑b : ℝ) ^ N * r ^ N = (1 : ℝ).

    Uses library mul_pow, mul_comm, one_pow.

    Lean, line 158
      have bN : (b : ℝ) ^ N * r ^ N = 1 := by rw [← mul_pow, mul_comm, rb, one_pow]

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 158 at d69d9751de5a ↗

  46. key have (↑b : ℝ) ^ N * (r ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) ≤ r ^ k

    Leaves False, with key : (↑b : ℝ) ^ N * (r ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) ≤ r ^ k.

    Uses library mul_one.

    Lean, lines 159–165
      have key : (b : ℝ) ^ N * (r ^ (k + (N + 1)) * 2) ≤ r ^ k := by
    have e : (b : ℝ) ^ N * (r ^ (k + (N + 1)) * 2)
        = r ^ k * ((b : ℝ) ^ N * r ^ N) * (2 * r) := by ring
    rw [e, bN, mul_one]
    have h2r : 2 * r ≤ 1 := by linarith
    calc r ^ k * (2 * r) ≤ r ^ k * 1 := mul_le_mul_of_nonneg_left h2r (pow_nonneg r0.le k)
      _ = r ^ k := mul_one _

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 159–165 at d69d9751de5a ↗

    1. key.e have (↑b : ℝ) ^ N * (r ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) = r ^ k * ((↑b : ℝ) ^ N * r ^ N) * ((2 : ℝ) * r) routine: ring

      Leaves (↑b : ℝ) ^ N * (r ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) ≤ r ^ k, with e : (↑b : ℝ) ^ N * (r ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) = r ^ k * ((↑b : ℝ) ^ N * r ^ N) * ((2 : ℝ) * r).

      Lean, lines 160–161
          have e : (b : ℝ) ^ N * (r ^ (k + (N + 1)) * 2)
        = r ^ k * ((b : ℝ) ^ N * r ^ N) * (2 * r) := by ring

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 160–161 at d69d9751de5a ↗

    2. key.h2r have (2 : ℝ) * r ≤ (1 : ℝ) routine: linarith

      Leaves r ^ k * ((2 : ℝ) * r) ≤ r ^ k, with h2r : (2 : ℝ) * r ≤ (1 : ℝ).

      Lean, line 163
          have h2r : 2 * r ≤ 1 := by linarith

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 163 at d69d9751de5a ↗

    3. key.s3 calc r ^ k * ((2 : ℝ) * r) ≤ r ^ k * (1 : ℝ)

      Closes the goal.

      Uses library mul_le_mul_of_nonneg_left, pow_nonneg.

      Lean, line 164
          calc r ^ k * (2 * r) ≤ r ^ k * 1 := mul_le_mul_of_nonneg_left h2r (pow_nonneg r0.le k)

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 164 at d69d9751de5a ↗

    4. key.s4 calc r ^ k * (1 : ℝ) = r ^ k

      Closes the goal.

      Uses library mul_one.

      Lean, line 165
            _ = r ^ k := mul_one _

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 165 at d69d9751de5a ↗

  47. s47 obtain ∃ (Z : ℕ), Z = ∑ i ∈ Finset.range (N + (1 : ℕ)), if (ω : ℕ → ℕ) i = m then b ^ (N - i) else (0 : ℕ)

    Leaves False, with Z : ℕ, hZ : Z = ∑ i ∈ Finset.range (N + (1 : ℕ)), if (ω : ℕ → ℕ) i = m then b ^ (N - i) else (0 : ℕ).

    Uses library Finset.range range n is the set of natural numbers less than n. , Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, lines 166–167
      obtain ⟨Z, hZ⟩ : ∃ Z : ℕ,
      Z = ∑ i ∈ Finset.range (N + 1), if ω i = m then b ^ (N - i) else 0 := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 166–167 at d69d9751de5a ↗

  48. hZ' have (↑b : ℝ) ^ N * ∑ i ∈ Finset.range (N + (1 : ℕ)), f i = (↑Z : ℝ)

    Leaves False, with hZ' : (↑b : ℝ) ^ N * ∑ i ∈ Finset.range (N + (1 : ℕ)), f i = (↑Z : ℝ).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.mul_sum, Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, lines 168–178
      have hZ' : (b : ℝ) ^ N * ∑ i ∈ Finset.range (N + 1), f i = (Z : ℝ) := by
    rw [hZ, Finset.mul_sum]; push_cast
    apply Finset.sum_congr rfl
    intro i hi
    have hi' : i ≤ N := Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)
    simp only [hf]
    split_ifs
    · have e : (b : ℝ) ^ N = (b : ℝ) ^ (N - i) * (b : ℝ) ^ i := by
        rw [← pow_add, Nat.sub_add_cancel hi']
      rw [e, mul_assoc, ← mul_pow, mul_comm (b : ℝ) r, rb, one_pow, mul_one]
    · simp

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 168–178 at d69d9751de5a ↗

    1. hZ'.hi' have i ≤ N

      Leaves (↑b : ℝ) ^ N * f i = if (ω : ℕ → ℕ) i = m then (↑b : ℝ) ^ (N - i) else (0 : ℝ), with hi' : i ≤ N.

      Uses library Nat.lt_succ_iff, Finset.mem_range.

      Lean, line 172
          have hi' : i ≤ N := Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 172 at d69d9751de5a ↗

    2. hZ'.s2 case

      Leaves (↑b : ℝ) ^ N * r ^ i = (↑b : ℝ) ^ (N - i).

      Uses library mul_assoc, mul_pow, mul_comm, one_pow, mul_one.

      Lean, lines 175–177
          · have e : (b : ℝ) ^ N = (b : ℝ) ^ (N - i) * (b : ℝ) ^ i := by
        rw [← pow_add, Nat.sub_add_cancel hi']
      rw [e, mul_assoc, ← mul_pow, mul_comm (b : ℝ) r, rb, one_pow, mul_one]

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 175–177 at d69d9751de5a ↗

      1. hZ'.s2.e have (↑b : ℝ) ^ N = (↑b : ℝ) ^ (N - i) * (↑b : ℝ) ^ i

        Leaves (↑b : ℝ) ^ N * r ^ i = (↑b : ℝ) ^ (N - i), with e : (↑b : ℝ) ^ N = (↑b : ℝ) ^ (N - i) * (↑b : ℝ) ^ i.

        Uses library pow_add, Nat.sub_add_cancel.

        Lean, lines 175–176
            · have e : (b : ℝ) ^ N = (b : ℝ) ^ (N - i) * (b : ℝ) ^ i := by
        rw [← pow_add, Nat.sub_add_cancel hi']

        targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 175–176 at d69d9751de5a ↗

    3. hZ'.s3 case routine: simp

      Leaves (↑b : ℝ) ^ N * (0 : ℝ) = (0 : ℝ).

      Lean, line 178
          · simp

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 178 at d69d9751de5a ↗

  49. hqk have (↑q : ℝ) * (↑k : ℝ) = (↑q.num : ℝ)

    Leaves False, with hqk : (↑q : ℝ) * (↑k : ℝ) = (↑q.num : ℝ).

    Uses library Rat.mul_den_eq_num.

    Lean, line 179
      have hqk : (q : ℝ) * k = q.num := by rw [hk]; exact_mod_cast Rat.mul_den_eq_num q

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 179 at d69d9751de5a ↗

  50. hx have (↑q : ℝ) = ∑ i ∈ Finset.range (N + (1 : ℕ)), f i + R

    Leaves False, with hx : (↑q : ℝ) = ∑ i ∈ Finset.range (N + (1 : ℕ)), f i + R.

    Uses library Finset.range range n is the set of natural numbers less than n. .

    Lean, lines 180–181
      have hx : (q : ℝ) = ∑ i ∈ Finset.range (N + 1), f i + R := by
    rw [hq, ← split1, split2']

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 180–181 at d69d9751de5a ↗

  51. hm have (↑((↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) = (↑k : ℝ) * ((↑b : ℝ) ^ N * R)

    Leaves False, with hm : (↑((↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) = (↑k : ℝ) * ((↑b : ℝ) ^ N * R).

    Lean, lines 182–184
      have hm : (((b : ℤ) ^ N * q.num - k * Z : ℤ) : ℝ) = (k : ℝ) * ((b : ℝ) ^ N * R) := by
    push_cast
    rw [← hqk, hx, ← hZ']; ring

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 182–184 at d69d9751de5a ↗

  52. kR have (0 : ℝ) < (↑k : ℝ)

    Leaves False, with kR : (0 : ℝ) < (↑k : ℝ).

    Lean, line 185
      have kR : (0 : ℝ) < k := by exact_mod_cast kpos

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 185 at d69d9751de5a ↗

  53. mpos have (0 : ℝ) < (↑((↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ)

    Leaves False, with mpos : (0 : ℝ) < (↑((↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ).

    Uses library mul_pos Alias of Left.mul_pos. , pow_pos.

    Lean, lines 186–187
      have mpos : (0 : ℝ) < (((b : ℤ) ^ N * q.num - k * Z : ℤ) : ℝ) := by
    rw [hm]; exact mul_pos kR (mul_pos (pow_pos bpos N) Rpos)

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 186–187 at d69d9751de5a ↗

  54. mlt have (↑((↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) < (1 : ℝ)

    Leaves False, with mlt : (↑((↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) < (1 : ℝ).

    Lean, lines 188–199
      have mlt : (((b : ℤ) ^ N * q.num - k * Z : ℤ) : ℝ) < 1 := by
    rw [hm]
    have h2 : (b : ℝ) ^ N * R ≤ r ^ k :=
      le_trans (mul_le_mul_of_nonneg_left Rle (pow_nonneg bpos.le N)) key
    have hk2 : (k : ℝ) < 2 ^ k := by exact_mod_cast Nat.lt_two_pow_self
    have hkb : (k : ℝ) * r ^ k < 1 := by
      have e : (k : ℝ) * r ^ k = k / (b : ℝ) ^ k := by rw [hr, div_pow, one_pow, mul_one_div]
      rw [e, div_lt_one (pow_pos bpos k)]
      calc (k : ℝ) < 2 ^ k := hk2
        _ ≤ (b : ℝ) ^ k := pow_le_pow_left₀ (by norm_num) hb0 k
    calc (k : ℝ) * ((b : ℝ) ^ N * R) ≤ k * r ^ k := mul_le_mul_of_nonneg_left h2 kR.le
      _ < 1 := hkb

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 188–199 at d69d9751de5a ↗

    1. mlt.h2 have (↑b : ℝ) ^ N * R ≤ r ^ k

      Leaves (↑k : ℝ) * ((↑b : ℝ) ^ N * R) < (1 : ℝ), with h2 : (↑b : ℝ) ^ N * R ≤ r ^ k.

      Uses library le_trans The relation ≤ on a preorder is transitive. , mul_le_mul_of_nonneg_left, pow_nonneg.

      Lean, lines 190–191
          have h2 : (b : ℝ) ^ N * R ≤ r ^ k :=
      le_trans (mul_le_mul_of_nonneg_left Rle (pow_nonneg bpos.le N)) key

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 190–191 at d69d9751de5a ↗

    2. mlt.hk2 have (↑k : ℝ) < (2 : ℝ) ^ k

      Leaves (↑k : ℝ) * ((↑b : ℝ) ^ N * R) < (1 : ℝ), with hk2 : (↑k : ℝ) < (2 : ℝ) ^ k.

      Uses library Nat.lt_two_pow_self.

      Lean, line 192
          have hk2 : (k : ℝ) < 2 ^ k := by exact_mod_cast Nat.lt_two_pow_self

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 192 at d69d9751de5a ↗

    3. mlt.hkb have (↑k : ℝ) * r ^ k < (1 : ℝ)

      Leaves (↑k : ℝ) * ((↑b : ℝ) ^ N * R) < (1 : ℝ), with hkb : (↑k : ℝ) * r ^ k < (1 : ℝ).

      Uses library div_lt_one, pow_pos.

      Lean, lines 193–197
          have hkb : (k : ℝ) * r ^ k < 1 := by
      have e : (k : ℝ) * r ^ k = k / (b : ℝ) ^ k := by rw [hr, div_pow, one_pow, mul_one_div]
      rw [e, div_lt_one (pow_pos bpos k)]
      calc (k : ℝ) < 2 ^ k := hk2
        _ ≤ (b : ℝ) ^ k := pow_le_pow_left₀ (by norm_num) hb0 k

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, lines 193–197 at d69d9751de5a ↗

      1. mlt.hkb.e have (↑k : ℝ) * r ^ k = (↑k : ℝ) / (↑b : ℝ) ^ k

        Leaves (↑k : ℝ) * r ^ k < (1 : ℝ), with e : (↑k : ℝ) * r ^ k = (↑k : ℝ) / (↑b : ℝ) ^ k.

        Uses library div_pow, one_pow, mul_one_div.

        Lean, line 194
              have e : (k : ℝ) * r ^ k = k / (b : ℝ) ^ k := by rw [hr, div_pow, one_pow, mul_one_div]

        targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 194 at d69d9751de5a ↗

      2. mlt.hkb.s2 calc (↑k : ℝ) < (2 : ℝ) ^ k

        Closes the goal.

        Lean, line 196
              calc (k : ℝ) < 2 ^ k := hk2

        targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 196 at d69d9751de5a ↗

      3. mlt.hkb.s3 calc (2 : ℝ) ^ k ≤ (↑b : ℝ) ^ k

        Closes the goal.

        Uses library pow_le_pow_left₀.

        Lean, line 197
                _ ≤ (b : ℝ) ^ k := pow_le_pow_left₀ (by norm_num) hb0 k

        targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 197 at d69d9751de5a ↗

    4. mlt.s4 calc (↑k : ℝ) * ((↑b : ℝ) ^ N * R) ≤ (↑k : ℝ) * r ^ k

      Closes the goal.

      Uses library mul_le_mul_of_nonneg_left.

      Lean, line 198
          calc (k : ℝ) * ((b : ℝ) ^ N * R) ≤ k * r ^ k := mul_le_mul_of_nonneg_left h2 kR.le

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 198 at d69d9751de5a ↗

    5. mlt.s5 calc (↑k : ℝ) * r ^ k < (1 : ℝ)

      Closes the goal.

      Lean, line 199
            _ < 1 := hkb

      targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 199 at d69d9751de5a ↗

  55. i1 have (0 : ℤ) < (↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)

    Leaves False, with i1 : (0 : ℤ) < (↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ).

    Lean, line 200
      have i1 : (0 : ℤ) < (b : ℤ) ^ N * q.num - k * Z := by exact_mod_cast mpos

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 200 at d69d9751de5a ↗

  56. i2 have (↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ) < (1 : ℤ)

    Leaves False, with i2 : (↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ) < (1 : ℤ).

    Lean, line 201
      have i2 : (b : ℤ) ^ N * q.num - k * Z < 1 := by exact_mod_cast mlt

    targets/erdos-69/nodes/variant-14c6c771/Proof.lean, line 201 at d69d9751de5a ↗

The proof in Lean (Proof.lean)

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

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-69/nodes/variant-14c6c771/Proof.lean, sha256 aab87793a8c0.
import Mathlib
import Nodes.«variant-14c6c771».Context

/-! A related variant of Erdős problem 69 (D-30, relation `related`): for every `m ≥ 1`, the
binary number whose n-th digit is 1 exactly when `ω n = m` is irrational.

Why it sits beside erdos-69: the root's number is `∑ ω(n)/2^n = ∑_{m ≥ 1} m · x_m`, where `x_m`
is the binary number of the level set `ω = m`; this node proves every `x_m` irrational. (`m = 0`
is excluded because `ω n = 0` only for `n = 0, 1`, giving `3/2`.) Method: by the Chinese
remainder theorem, for any `k` there are `k` consecutive integers each divisible by `m + 1`
fixed primes of its own, so each has `ω ≥ m + 1`: a window of `k` zero digits; and the powers
of a product of `m` primes give infinitely many 1 digits. If `x_m = a/k` then `k · 2^N · (tail
after the window)` is an integer strictly between 0 and 1. It does not reach the root: an
irrational combination of irrationals can be rational, and the root's digits have no window of
zeros. -/

open scoped ArithmeticFunction.omega

theorem Opn.erdos_69_omega_level_sets :
    ∀ m : ℕ, 1 ≤ m → Irrational (∑' n : ℕ, if ω n = m then (1 / 2 : ℝ) ^ n else 0) := by
  intro m hm
  have hω : ∀ n : ℕ, ω n = n.primeFactors.card := fun n => by
    rw [ArithmeticFunction.cardDistinctFactors_apply, ← List.card_toFinset]; rfl
  have Pinj : Function.Injective (Nat.nth Nat.Prime) := Nat.nth_injective Nat.infinite_setOfPred_prime
  -- `T j c`: the `c` primes with indices `(j, 0), …, (j, c - 1)`, disjoint for distinct `j`
  obtain ⟨T, hT⟩ : ∃ T : ℕ → ℕ → Finset ℕ, ∀ j c,
      T j c = (Finset.range c).image (fun i => Nat.nth Nat.Prime (Nat.pair j i)) :=
    ⟨fun j c => _, fun _ _ => rfl⟩
  have T_prime : ∀ j c, ∀ p ∈ T j c, p.Prime := by
    intro j c p hp
    rw [hT] at hp
    obtain ⟨i, -, rfl⟩ := Finset.mem_image.mp hp
    exact Nat.prime_nth_prime _
  have T_card : ∀ j c, (T j c).card = c := by
    intro j c
    rw [hT, Finset.card_image_of_injective _ (fun a b h => (Nat.pair_eq_pair.mp (Pinj h)).2),
      Finset.card_range]
  have T_disj : ∀ j j' c c', j ≠ j' → ∀ p ∈ T j c, ∀ q ∈ T j' c', p ≠ q := by
    intro j j' c c' hjj p hp q hq hpq
    rw [hT] at hp hq
    obtain ⟨i, -, rfl⟩ := Finset.mem_image.mp hp
    obtain ⟨i', -, rfl⟩ := Finset.mem_image.mp hq
    exact hjj (Nat.pair_eq_pair.mp (Pinj hpq)).1
  have prod_pf : ∀ j c, (∏ p ∈ T j c, p).primeFactors = T j c :=
    fun j c => Nat.primeFactors_prod (T_prime j c)
  -- `Q j`: a product of `m + 1` primes, pairwise coprime for distinct `j`
  obtain ⟨Q, hQ⟩ : ∃ Q : ℕ → ℕ, ∀ j, Q j = ∏ p ∈ T j (m + 1), p := ⟨fun j => _, fun _ => rfl⟩
  have Qpos : ∀ j, 0 < Q j := fun j => by
    rw [hQ]; exact Finset.prod_pos (fun p hp => (T_prime j (m + 1) p hp).pos)
  have Qcop : ∀ j j', j ≠ j' → Nat.Coprime (Q j) (Q j') := by
    intro j j' hjj
    rw [hQ j, hQ j']
    apply Nat.Coprime.prod_left
    intro p hp
    apply Nat.Coprime.prod_right
    intro q hq
    exact (Nat.coprime_primes (T_prime _ _ p hp) (T_prime _ _ q hq)).mpr
      (T_disj j j' _ _ hjj p hp q hq)
  -- a window of `k` places, each with at least `m + 1` prime factors (Chinese remainder theorem)
  have window : ∀ k : ℕ, ∃ N : ℕ, ∀ j, j < k → ω (j + (N + 1)) ≠ m := by
    intro k
    obtain ⟨N, hN⟩ := Nat.chineseRemainderOfFinset (fun j => Q j - (j + 1) % Q j) Q
      (Finset.range k) (fun j _ => (Qpos j).ne') (fun j _ j' _ hjj => Qcop j j' hjj)
    refine ⟨N, fun j hj => ?_⟩
    have hmod := hN j (Finset.mem_range.mpr hj)
    have hdvd : Q j ∣ j + (N + 1) := by
      have h1 : N + (j + 1) ≡ (Q j - (j + 1) % Q j) + (j + 1) % Q j [MOD Q j] :=
        Nat.ModEq.add hmod (Nat.mod_modEq (j + 1) (Q j)).symm
      rw [Nat.sub_add_cancel (Nat.mod_lt _ (Qpos j)).le] at h1
      have h2 : N + (j + 1) ≡ 0 [MOD Q j] := h1.trans (Nat.modEq_zero_iff_dvd.mpr dvd_rfl)
      have h3 := Nat.modEq_zero_iff_dvd.mp h2
      rwa [show j + (N + 1) = N + (j + 1) by ring]
    have hsub : T j (m + 1) ⊆ (j + (N + 1)).primeFactors := by
      rw [← prod_pf j (m + 1), ← hQ]
      exact Nat.primeFactors_mono hdvd (by omega)
    have hcard := Finset.card_le_card hsub
    rw [T_card] at hcard
    rw [hω]; omega
  -- infinitely many `n` with exactly `m` prime factors: the powers of a product of `m` primes
  obtain ⟨W, hW⟩ : ∃ W : ℕ, W = ∏ p ∈ T 0 m, p := ⟨_, rfl⟩
  have Wc : W.primeFactors.card = m := by rw [hW, prod_pf, T_card]
  have W2 : 2 ≤ W := by
    rcases Nat.lt_or_ge W 2 with h | h
    · interval_cases W <;> simp at Wc <;> omega
    · exact h
  have many : ∀ L : ℕ, ∃ n, L ≤ n ∧ ω n = m := by
    intro L
    refine ⟨W ^ (L + 1), ?_, ?_⟩
    · calc L ≤ 2 ^ L := Nat.lt_two_pow_self.le
        _ ≤ 2 ^ (L + 1) := Nat.pow_le_pow_right (by norm_num) (by omega)
        _ ≤ W ^ (L + 1) := Nat.pow_le_pow_left W2 _
    · rw [hω, Nat.primeFactors_pow _ (by omega), Wc]
  obtain ⟨b, hbdef⟩ : ∃ b : ℕ, b = 2 := ⟨_, rfl⟩
  have hb : 2 ≤ b := by omega
  have hb0 : (2 : ℝ) ≤ (b : ℝ) := by exact_mod_cast hb
  have bpos : (0 : ℝ) < b := by linarith
  obtain ⟨r, hr⟩ : ∃ r : ℝ, r = 1 / (b : ℝ) := ⟨_, rfl⟩
  have r0 : 0 < r := by rw [hr]; exact one_div_pos.mpr bpos
  have r2 : r ≤ 1 / 2 := by rw [hr]; exact one_div_le_one_div_of_le (by norm_num) hb0
  have rb : r * (b : ℝ) = 1 := by rw [hr, one_div, inv_mul_cancel₀ bpos.ne']
  have r12 : r = 1 / 2 := by rw [hr, hbdef]; norm_num
  obtain ⟨f, hf⟩ : ∃ f : ℕ → ℝ, f = fun n => if ω n = m then r ^ n else 0 := ⟨_, rfl⟩
  have hconv : (∑' n : ℕ, if ω n = m then (1 / 2 : ℝ) ^ n else 0) = ∑' n : ℕ, f n := by
    simp only [hf, r12]
  rw [hconv]
  have f_nonneg : ∀ n, 0 ≤ f n := fun n => by
    simp only [hf]; split_ifs
    · exact pow_nonneg r0.le n
    · exact le_rfl
  have f_le : ∀ n, f n ≤ r ^ n := fun n => by
    simp only [hf]; split_ifs
    · exact le_rfl
    · exact pow_nonneg r0.le n
  have hs : Summable f :=
    Summable.of_nonneg_of_le f_nonneg f_le
      (summable_geometric_of_lt_one r0.le (by linarith))
  rintro ⟨q, hq⟩
  obtain ⟨k, hk⟩ : ∃ k, k = q.den := ⟨_, rfl⟩
  have kpos : 0 < k := by rw [hk]; exact q.den_pos
  obtain ⟨N, hNw⟩ := window k
  have comp : ∀ j, j < k → f (j + (N + 1)) = 0 := by
    intro j hj
    simp only [hf]
    rw [if_neg (hNw j hj)]
  have hg : Summable (fun i => f (i + (N + 1))) := (summable_nat_add_iff (N + 1)).mpr hs
  have hg' : Summable (fun i => f (i + k + (N + 1))) := by
    have := (summable_nat_add_iff k).mpr hg
    simpa [add_assoc] using this
  have split1 := Summable.sum_add_tsum_nat_add (N + 1) hs
  have split2 := Summable.sum_add_tsum_nat_add k hg
  have zero_part : ∑ i ∈ Finset.range k, f (i + (N + 1)) = 0 := by
    apply Finset.sum_eq_zero
    intro j hj
    exact comp j (Finset.mem_range.mp hj)
  obtain ⟨R, hR⟩ : ∃ R, R = ∑' i, f (i + k + (N + 1)) := ⟨_, rfl⟩
  have split2' : ∑' i, f (i + (N + 1)) = R := by
    rw [← split2, zero_part, zero_add, hR]
  have Rpos : 0 < R := by
    obtain ⟨p, hp1, hp2⟩ := many (k + (N + 1))
    have hpi : p - (k + (N + 1)) + k + (N + 1) = p := by omega
    rw [hR]
    refine hg'.tsum_pos (fun i => f_nonneg _) (p - (k + (N + 1))) ?_
    rw [hpi]; simp only [hf, if_pos hp2]
    exact pow_pos r0 p
  have geo : Summable (fun i : ℕ => r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i) :=
    summable_geometric_two.mul_left _
  have term_le : ∀ i, f (i + k + (N + 1)) ≤ r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i := by
    intro i
    calc f (i + k + (N + 1)) ≤ r ^ (i + k + (N + 1)) := f_le _
      _ = r ^ (k + (N + 1)) * r ^ i := by ring
      _ ≤ r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i :=
        mul_le_mul_of_nonneg_left (pow_le_pow_left₀ r0.le r2 i) (pow_nonneg r0.le _)
  have Rle : R ≤ r ^ (k + (N + 1)) * 2 := by
    rw [hR]
    calc ∑' i, f (i + k + (N + 1)) ≤ ∑' i : ℕ, r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i :=
          Summable.tsum_le_tsum term_le hg' geo
      _ = r ^ (k + (N + 1)) * 2 := by rw [tsum_mul_left, tsum_geometric_two]
  have bN : (b : ℝ) ^ N * r ^ N = 1 := by rw [← mul_pow, mul_comm, rb, one_pow]
  have key : (b : ℝ) ^ N * (r ^ (k + (N + 1)) * 2) ≤ r ^ k := by
    have e : (b : ℝ) ^ N * (r ^ (k + (N + 1)) * 2)
        = r ^ k * ((b : ℝ) ^ N * r ^ N) * (2 * r) := by ring
    rw [e, bN, mul_one]
    have h2r : 2 * r ≤ 1 := by linarith
    calc r ^ k * (2 * r) ≤ r ^ k * 1 := mul_le_mul_of_nonneg_left h2r (pow_nonneg r0.le k)
      _ = r ^ k := mul_one _
  obtain ⟨Z, hZ⟩ : ∃ Z : ℕ,
      Z = ∑ i ∈ Finset.range (N + 1), if ω i = m then b ^ (N - i) else 0 := ⟨_, rfl⟩
  have hZ' : (b : ℝ) ^ N * ∑ i ∈ Finset.range (N + 1), f i = (Z : ℝ) := by
    rw [hZ, Finset.mul_sum]; push_cast
    apply Finset.sum_congr rfl
    intro i hi
    have hi' : i ≤ N := Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)
    simp only [hf]
    split_ifs
    · have e : (b : ℝ) ^ N = (b : ℝ) ^ (N - i) * (b : ℝ) ^ i := by
        rw [← pow_add, Nat.sub_add_cancel hi']
      rw [e, mul_assoc, ← mul_pow, mul_comm (b : ℝ) r, rb, one_pow, mul_one]
    · simp
  have hqk : (q : ℝ) * k = q.num := by rw [hk]; exact_mod_cast Rat.mul_den_eq_num q
  have hx : (q : ℝ) = ∑ i ∈ Finset.range (N + 1), f i + R := by
    rw [hq, ← split1, split2']
  have hm : (((b : ℤ) ^ N * q.num - k * Z : ℤ) : ℝ) = (k : ℝ) * ((b : ℝ) ^ N * R) := by
    push_cast
    rw [← hqk, hx, ← hZ']; ring
  have kR : (0 : ℝ) < k := by exact_mod_cast kpos
  have mpos : (0 : ℝ) < (((b : ℤ) ^ N * q.num - k * Z : ℤ) : ℝ) := by
    rw [hm]; exact mul_pos kR (mul_pos (pow_pos bpos N) Rpos)
  have mlt : (((b : ℤ) ^ N * q.num - k * Z : ℤ) : ℝ) < 1 := by
    rw [hm]
    have h2 : (b : ℝ) ^ N * R ≤ r ^ k :=
      le_trans (mul_le_mul_of_nonneg_left Rle (pow_nonneg bpos.le N)) key
    have hk2 : (k : ℝ) < 2 ^ k := by exact_mod_cast Nat.lt_two_pow_self
    have hkb : (k : ℝ) * r ^ k < 1 := by
      have e : (k : ℝ) * r ^ k = k / (b : ℝ) ^ k := by rw [hr, div_pow, one_pow, mul_one_div]
      rw [e, div_lt_one (pow_pos bpos k)]
      calc (k : ℝ) < 2 ^ k := hk2
        _ ≤ (b : ℝ) ^ k := pow_le_pow_left₀ (by norm_num) hb0 k
    calc (k : ℝ) * ((b : ℝ) ^ N * R) ≤ k * r ^ k := mul_le_mul_of_nonneg_left h2 kR.le
      _ < 1 := hkb
  have i1 : (0 : ℤ) < (b : ℤ) ^ N * q.num - k * Z := by exact_mod_cast mpos
  have i2 : (b : ℤ) ^ N * q.num - k * Z < 1 := by exact_mod_cast mlt
  omega

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-14c6c771».Context

/-! A related variant of Erdős problem 69 (D-30, relation `related`): for every `m ≥ 1`, the
binary number whose n-th digit is 1 exactly when `ω n = m` is irrational.

Why it sits beside erdos-69: the root's number is `∑ ω(n)/2^n = ∑_{m ≥ 1} m · x_m`, where `x_m`
is the binary number of the level set `ω = m`; this node proves every `x_m` irrational. (`m = 0`
is excluded because `ω n = 0` only for `n = 0, 1`, giving `3/2`.) Method: by the Chinese
remainder theorem, for any `k` there are `k` consecutive integers each divisible by `m + 1`
fixed primes of its own, so each has `ω ≥ m + 1`: a window of `k` zero digits; and the powers
of a product of `m` primes give infinitely many 1 digits. If `x_m = a/k` then `k · 2^N · (tail
after the window)` is an integer strictly between 0 and 1. It does not reach the root: an
irrational combination of irrationals can be rational, and the root's digits have no window of
zeros. -/

open scoped ArithmeticFunction.omega

theorem Opn.erdos_69_omega_level_sets :
    ∀ m : ℕ, 1 ≤ m → Irrational (∑' n : ℕ, if ω n = m then (1 / 2 : ℝ) ^ n else 0) := by
  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 →

In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \forall m\in\mathbb{N},\ m\ge 1:\quad \sum_{n=0}^{\infty}\bigl[\omega(n)=m\bigr]\Bigl(\frac{1}{2}\Bigr)^{n} \notin\mathbb{Q}$

For every natural m ≥ 1, the real number with a binary 1 in place n exactly when n has m distinct prime factors, the sum over n ≥ 0 of (1/2)^n when ω(n) = m and 0 otherwise, is irrational. The series is a tsum over ℝ (0 when not summable), and Irrational x means x is not the cast of a rational.

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

Rendered from targets/erdos-69/nodes/variant-14c6c771/Statement.lean. Origin: variant (related).

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000308.json, merge commit d69d9751de5a.

Verdict pass, from attestations/000308.json.

Submitter
t0929-3
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
none needed (calibration)
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

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

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-69/nodes/variant-14c6c771/Witness.lean, sha256 d4dabaeca88e.
theorem witness : ∃ m : ℕ, 1 ≤ m := ⟨1, le_rfl⟩

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 →

Acknowledged findings (1)

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

Untrusted: acknowledgment of a off-by-one-range finding at 1 ≤ m

Inclusive on purpose: m = 0 must be excluded, since ω n = 0 only for n = 0 and n = 1 and that level set's number is 3/2, rational; every m ≥ 1 is claimed.

How to read this page

How to read a statement’s page →