Open Proof Network

Problems / erdos-69 / spec-e0b917d1

Reciprocal prime mass of a rough dilation

spec-e0b917d1 Opn.erdos_69_rough_dilation_reciprocal

proved

Proposed by a contributor.

$\displaystyle \forall P,j\in\mathbb{N},\ 2\le P,\ j\le P:\quad \sum_{p\mid 1+P\#\,(1+j)}\frac{1}{p} \le \frac{5}{\log P}$

For naturals P ≥ 2 and j ≤ P, the sum of 1/p over the prime factors p of 1 + P#·(1+j) is at most 5/log P, where P# is the primorial (the product of the primes at most P), the sum runs over (…).primeFactors, and log is the natural logarithm, all in ℝ.

unverified · history

Lean
theorem Opn.erdos_69_rough_dilation_reciprocal :
    ∀ P j : ℕ, 2 ≤ P → j ≤ P →
      ∑ p ∈ (1 + primorial P * (1 + j)).primeFactors, (1 : ℝ) / p ≤ 5 / Real.log P := 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, 000310, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000310.json, merge commit 0790c5bd2b57.

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. ha0 have a ≠ (0 : ℕ) routine: omega

    Leaves ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ (5 : ℝ) / Real.log (↑P : ℝ), with ha0 : a ≠ (0 : ℕ).

    Lean, line 16
      have ha0 : a ≠ 0 := by omega

    targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 16 at 0790c5bd2b57 ↗

  2. hbig have ∀ p ∈ a.primeFactors, P < p

    Leaves ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ (5 : ℝ) / Real.log (↑P : ℝ), with hbig : ∀ p ∈ a.primeFactors, P < p.

    Uses library Not Not p, or ¬p, is the negation of p. , Nat.dvd_one.

    Lean, lines 18–30
      have hbig : ∀ p ∈ a.primeFactors, P < p := by
    intro p hp
    have hpp : p.Prime := Nat.prime_of_mem_primeFactors hp
    have hpd : p ∣ a := Nat.dvd_of_mem_primeFactors hp
    by_contra hle
    push Not at hle
    have hprim : p ∣ primorial P := by
      apply Finset.dvd_prod_of_mem
      rw [Finset.mem_filter, Finset.mem_range]
      exact ⟨by omega, hpp⟩
    have hpd' : p ∣ primorial P * (1 + j) + 1 := by rw [add_comm]; exact hpd
    have h1 : p ∣ 1 := (Nat.dvd_add_right (dvd_mul_of_dvd_left hprim (1 + j))).mp hpd'
    exact hpp.one_lt.ne' (Nat.dvd_one.mp h1)

    targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 18–30 at 0790c5bd2b57 ↗

    1. hbig.hpp have Nat.Prime p

      Leaves P < p, with hpp : Nat.Prime p.

      Uses library Nat.prime_of_mem_primeFactors.

      Lean, line 20
          have hpp : p.Prime := Nat.prime_of_mem_primeFactors hp

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 20 at 0790c5bd2b57 ↗

    2. hbig.hpd have p ∣ a

      Leaves P < p, with hpd : p ∣ a.

      Uses library Nat.dvd_of_mem_primeFactors.

      Lean, line 21
          have hpd : p ∣ a := Nat.dvd_of_mem_primeFactors hp

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 21 at 0790c5bd2b57 ↗

    3. hbig.hprim have p ∣ primorial P

      Leaves False, with hprim : p ∣ primorial P.

      Uses library primorial The primorial n# of n is the product of the primes less than or equal to n. , Finset.dvd_prod_of_mem, Finset.mem_filter, Finset.mem_range, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

      Lean, lines 24–27
          have hprim : p ∣ primorial P := by
      apply Finset.dvd_prod_of_mem
      rw [Finset.mem_filter, Finset.mem_range]
      exact ⟨by omega, hpp⟩

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 24–27 at 0790c5bd2b57 ↗

    4. hbig.hpd' have p ∣ primorial P * ((1 : ℕ) + j) + (1 : ℕ)

      Leaves False, with hpd' : p ∣ primorial P * ((1 : ℕ) + j) + (1 : ℕ).

      Uses library primorial The primorial n# of n is the product of the primes less than or equal to n. , add_comm.

      Lean, line 28
          have hpd' : p ∣ primorial P * (1 + j) + 1 := by rw [add_comm]; exact hpd

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 28 at 0790c5bd2b57 ↗

    5. hbig.h1 have p ∣ (1 : ℕ)

      Leaves False, with h1 : p ∣ (1 : ℕ).

      Uses library Nat.dvd_add_right, dvd_mul_of_dvd_left.

      Lean, line 29
          have h1 : p ∣ 1 := (Nat.dvd_add_right (dvd_mul_of_dvd_left hprim (1 + j))).mp hpd'

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 29 at 0790c5bd2b57 ↗

  3. hPpos have (0 : ℝ) < (↑P : ℝ)

    Leaves ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ (5 : ℝ) / Real.log (↑P : ℝ), with hPpos : (0 : ℝ) < (↑P : ℝ).

    Lean, line 32
      have hPpos : (0 : ℝ) < P := by exact_mod_cast (show 0 < P by omega)

    targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 32 at 0790c5bd2b57 ↗

  4. hlogP have (0 : ℝ) < Real.log (↑P : ℝ)

    Leaves ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ (5 : ℝ) / Real.log (↑P : ℝ), with hlogP : (0 : ℝ) < Real.log (↑P : ℝ).

    Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Real.log_pos.

    Lean, line 33
      have hlogP : 0 < Real.log P := Real.log_pos (by exact_mod_cast (show 1 < P by omega))

    targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 33 at 0790c5bd2b57 ↗

  5. hpow have (↑P : ℝ) ^ k ≤ (↑a : ℝ)

    Leaves ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ (5 : ℝ) / Real.log (↑P : ℝ), with hpow : (↑P : ℝ) ^ k ≤ (↑a : ℝ).

    Lean, lines 35–41
      have hpow : (P : ℝ) ^ k ≤ a := by
    have h1 : P ^ k ≤ ∏ p ∈ a.primeFactors, p := by
      rw [hk]
      exact Finset.pow_card_le_prod _ _ _ (fun p hp => (hbig p hp).le)
    have h2 : ∏ p ∈ a.primeFactors, p ≤ a :=
      Nat.le_of_dvd (Nat.pos_of_ne_zero ha0) (Nat.prod_primeFactors_dvd a)
    exact_mod_cast h1.trans h2

    targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 35–41 at 0790c5bd2b57 ↗

    1. hpow.h1 have P ^ k ≤ ∏ p ∈ a.primeFactors, p

      Leaves (↑P : ℝ) ^ k ≤ (↑a : ℝ), with h1 : P ^ k ≤ ∏ p ∈ a.primeFactors, p.

      Uses library Finset.pow_card_le_prod.

      Lean, lines 36–38
          have h1 : P ^ k ≤ ∏ p ∈ a.primeFactors, p := by
      rw [hk]
      exact Finset.pow_card_le_prod _ _ _ (fun p hp => (hbig p hp).le)

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 36–38 at 0790c5bd2b57 ↗

    2. hpow.h2 have ∏ p ∈ a.primeFactors, p ≤ a

      Leaves (↑P : ℝ) ^ k ≤ (↑a : ℝ), with h2 : ∏ p ∈ a.primeFactors, p ≤ a.

      Uses library Nat.le_of_dvd, Nat.pos_of_ne_zero, Nat.prod_primeFactors_dvd.

      Lean, lines 39–40
          have h2 : ∏ p ∈ a.primeFactors, p ≤ a :=
      Nat.le_of_dvd (Nat.pos_of_ne_zero ha0) (Nat.prod_primeFactors_dvd a)

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 39–40 at 0790c5bd2b57 ↗

  6. ha16 have a ≤ (16 : ℕ) ^ P

    Leaves ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ (5 : ℝ) / Real.log (↑P : ℝ), with ha16 : a ≤ (16 : ℕ) ^ P.

    Lean, lines 43–51
      have ha16 : a ≤ 16 ^ P := by
    have h4 : primorial P ≤ 4 ^ P := primorial_le_four_pow P
    have h2 : P + 2 ≤ 4 ^ P := by
      have : P < 2 ^ P := Nat.lt_two_pow_self
      have : 4 ^ P = 2 ^ P * 2 ^ P := by rw [← mul_pow]; norm_num
      nlinarith [Nat.one_le_two_pow (n := P)]
    have h16 : 16 ^ P = 4 ^ P * 4 ^ P := by rw [← mul_pow]; norm_num
    have : primorial P * (1 + j) ≤ 4 ^ P * (1 + P) := Nat.mul_le_mul h4 (by omega)
    nlinarith

    targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 43–51 at 0790c5bd2b57 ↗

    1. ha16.h4 have primorial P ≤ (4 : ℕ) ^ P

      Leaves a ≤ (16 : ℕ) ^ P, with h4 : primorial P ≤ (4 : ℕ) ^ P.

      Uses library primorial The primorial n# of n is the product of the primes less than or equal to n. , primorial_le_four_pow.

      Lean, line 44
          have h4 : primorial P ≤ 4 ^ P := primorial_le_four_pow P

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 44 at 0790c5bd2b57 ↗

    2. ha16.h2 have P + (2 : ℕ) ≤ (4 : ℕ) ^ P

      Leaves a ≤ (16 : ℕ) ^ P, with h2 : P + (2 : ℕ) ≤ (4 : ℕ) ^ P.

      Uses library Nat.one_le_two_pow.

      Lean, lines 45–48
          have h2 : P + 2 ≤ 4 ^ P := by
      have : P < 2 ^ P := Nat.lt_two_pow_self
      have : 4 ^ P = 2 ^ P * 2 ^ P := by rw [← mul_pow]; norm_num
      nlinarith [Nat.one_le_two_pow (n := P)]

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 45–48 at 0790c5bd2b57 ↗

      1. ha16.h2.s1 have P < (2 : ℕ) ^ P

        Leaves P + (2 : ℕ) ≤ (4 : ℕ) ^ P, with this : P < (2 : ℕ) ^ P.

        Uses library Nat.lt_two_pow_self.

        Lean, line 46
              have : P < 2 ^ P := Nat.lt_two_pow_self

        targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 46 at 0790c5bd2b57 ↗

      2. ha16.h2.s2 have (4 : ℕ) ^ P = (2 : ℕ) ^ P * (2 : ℕ) ^ P

        Leaves P + (2 : ℕ) ≤ (4 : ℕ) ^ P, with this : (4 : ℕ) ^ P = (2 : ℕ) ^ P * (2 : ℕ) ^ P.

        Uses library mul_pow.

        Lean, line 47
              have : 4 ^ P = 2 ^ P * 2 ^ P := by rw [← mul_pow]; norm_num

        targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 47 at 0790c5bd2b57 ↗

    3. ha16.h16 have (16 : ℕ) ^ P = (4 : ℕ) ^ P * (4 : ℕ) ^ P

      Leaves a ≤ (16 : ℕ) ^ P, with h16 : (16 : ℕ) ^ P = (4 : ℕ) ^ P * (4 : ℕ) ^ P.

      Uses library mul_pow.

      Lean, line 49
          have h16 : 16 ^ P = 4 ^ P * 4 ^ P := by rw [← mul_pow]; norm_num

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 49 at 0790c5bd2b57 ↗

    4. ha16.this have primorial P * ((1 : ℕ) + j) ≤ (4 : ℕ) ^ P * ((1 : ℕ) + P)

      Leaves a ≤ (16 : ℕ) ^ P, with this : primorial P * ((1 : ℕ) + j) ≤ (4 : ℕ) ^ P * ((1 : ℕ) + P).

      Uses library primorial The primorial n# of n is the product of the primes less than or equal to n. , Nat.mul_le_mul.

      Lean, line 50
          have : primorial P * (1 + j) ≤ 4 ^ P * (1 + P) := Nat.mul_le_mul h4 (by omega)

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 50 at 0790c5bd2b57 ↗

  7. hloga have Real.log (↑a : ℝ) ≤ (5 : ℝ) * (↑P : ℝ)

    Leaves ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ (5 : ℝ) / Real.log (↑P : ℝ), with hloga : Real.log (↑a : ℝ) ≤ (5 : ℝ) * (↑P : ℝ).

    Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. .

    Lean, lines 53–67
      have hloga : Real.log a ≤ 5 * P := by
    have hapos : (0 : ℝ) < a := by exact_mod_cast Nat.pos_of_ne_zero ha0
    have h16 : (a : ℝ) ≤ 16 ^ P := by exact_mod_cast ha16
    have he : (16 : ℝ) ≤ Real.exp 5 := by
      have h2 : (2 : ℝ) ≤ Real.exp 1 := by
        have := Real.add_one_le_exp (1 : ℝ); linarith
      have : Real.exp 5 = Real.exp 1 ^ 5 := by rw [← Real.exp_nat_mul]; norm_num
      rw [this]
      nlinarith [pow_le_pow_left₀ (by norm_num) h2 5]
    calc Real.log a ≤ Real.log (16 ^ P) := Real.log_le_log hapos h16
      _ = P * Real.log 16 := by rw [Real.log_pow]
      _ ≤ P * 5 := by
          apply mul_le_mul_of_nonneg_left _ hPpos.le
          rw [Real.log_le_iff_le_exp (by norm_num)]; exact he
      _ = 5 * P := by ring

    targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 53–67 at 0790c5bd2b57 ↗

    1. hloga.hapos have (0 : ℝ) < (↑a : ℝ)

      Leaves Real.log (↑a : ℝ) ≤ (5 : ℝ) * (↑P : ℝ), with hapos : (0 : ℝ) < (↑a : ℝ).

      Uses library Nat.pos_of_ne_zero.

      Lean, line 54
          have hapos : (0 : ℝ) < a := by exact_mod_cast Nat.pos_of_ne_zero ha0

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 54 at 0790c5bd2b57 ↗

    2. hloga.h16 have (↑a : ℝ) ≤ (16 : ℝ) ^ P

      Leaves Real.log (↑a : ℝ) ≤ (5 : ℝ) * (↑P : ℝ), with h16 : (↑a : ℝ) ≤ (16 : ℝ) ^ P.

      Lean, line 55
          have h16 : (a : ℝ) ≤ 16 ^ P := by exact_mod_cast ha16

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 55 at 0790c5bd2b57 ↗

    3. hloga.he have (16 : ℝ) ≤ Real.exp (5 : ℝ)

      Leaves Real.log (↑a : ℝ) ≤ (5 : ℝ) * (↑P : ℝ), with he : (16 : ℝ) ≤ Real.exp (5 : ℝ).

      Uses library Real.exp The real exponential function, defined as the real part of the complex exponential , pow_le_pow_left₀.

      Lean, lines 56–61
          have he : (16 : ℝ) ≤ Real.exp 5 := by
      have h2 : (2 : ℝ) ≤ Real.exp 1 := by
        have := Real.add_one_le_exp (1 : ℝ); linarith
      have : Real.exp 5 = Real.exp 1 ^ 5 := by rw [← Real.exp_nat_mul]; norm_num
      rw [this]
      nlinarith [pow_le_pow_left₀ (by norm_num) h2 5]

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 56–61 at 0790c5bd2b57 ↗

      1. hloga.he.h2 have (2 : ℝ) ≤ Real.exp (1 : ℝ)

        Leaves (16 : ℝ) ≤ Real.exp (5 : ℝ), with h2 : (2 : ℝ) ≤ Real.exp (1 : ℝ).

        Uses library Real.exp The real exponential function, defined as the real part of the complex exponential .

        Lean, lines 57–58
              have h2 : (2 : ℝ) ≤ Real.exp 1 := by
        have := Real.add_one_le_exp (1 : ℝ); linarith

        targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 57–58 at 0790c5bd2b57 ↗

        1. hloga.he.h2.this have (1 : ℝ) + (1 : ℝ) ≤ Real.exp (1 : ℝ)

          Leaves (2 : ℝ) ≤ Real.exp (1 : ℝ), with this : (1 : ℝ) + (1 : ℝ) ≤ Real.exp (1 : ℝ).

          Uses library Real.add_one_le_exp.

          Lean, line 58
                  have := Real.add_one_le_exp (1 : ℝ); linarith

          targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 58 at 0790c5bd2b57 ↗

      2. hloga.he.this have Real.exp (5 : ℝ) = Real.exp (1 : ℝ) ^ (5 : ℕ)

        Leaves (16 : ℝ) ≤ Real.exp (5 : ℝ), with this : Real.exp (5 : ℝ) = Real.exp (1 : ℝ) ^ (5 : ℕ).

        Uses library Real.exp The real exponential function, defined as the real part of the complex exponential , Real.exp_nat_mul.

        Lean, line 59
              have : Real.exp 5 = Real.exp 1 ^ 5 := by rw [← Real.exp_nat_mul]; norm_num

        targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 59 at 0790c5bd2b57 ↗

    4. hloga.s4 calc Real.log (↑a : ℝ) ≤ Real.log ((16 : ℝ) ^ P)

      Closes the goal.

      Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Real.log_le_log.

      Lean, line 62
          calc Real.log a ≤ Real.log (16 ^ P) := Real.log_le_log hapos h16

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 62 at 0790c5bd2b57 ↗

    5. hloga.s5 calc

      Closes the goal.

      Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Real.log_pow.

      Lean, line 63
            _ = P * Real.log 16 := by rw [Real.log_pow]

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 63 at 0790c5bd2b57 ↗

    6. hloga.s6 calc

      Closes the goal.

      Uses library mul_le_mul_of_nonneg_left, Real.log_le_iff_le_exp.

      Lean, lines 64–66
            _ ≤ P * 5 := by
          apply mul_le_mul_of_nonneg_left _ hPpos.le
          rw [Real.log_le_iff_le_exp (by norm_num)]; exact he

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 64–66 at 0790c5bd2b57 ↗

    7. hloga.s7 calc routine: ring

      Closes the goal.

      Lean, line 67
            _ = 5 * P := by ring

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 67 at 0790c5bd2b57 ↗

  8. hklog have (↑k : ℝ) * Real.log (↑P : ℝ) ≤ Real.log (↑a : ℝ)

    Leaves ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ (5 : ℝ) / Real.log (↑P : ℝ), with hklog : (↑k : ℝ) * Real.log (↑P : ℝ) ≤ Real.log (↑a : ℝ).

    Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , Real.log_pow.

    Lean, lines 69–71
      have hklog : (k : ℝ) * Real.log P ≤ Real.log a := by
    have := Real.log_le_log (by positivity) hpow
    rwa [Real.log_pow] at this

    targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 69–71 at 0790c5bd2b57 ↗

    1. hklog.this have Real.log ((↑P : ℝ) ^ k) ≤ Real.log (↑a : ℝ)

      Leaves (↑k : ℝ) * Real.log (↑P : ℝ) ≤ Real.log (↑a : ℝ), with this : Real.log ((↑P : ℝ) ^ k) ≤ Real.log (↑a : ℝ).

      Uses library Real.log_le_log.

      Lean, line 70
          have := Real.log_le_log (by positivity) hpow

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 70 at 0790c5bd2b57 ↗

  9. hsum have ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ (↑k : ℝ) * ((1 : ℝ) / (↑P : ℝ))

    Leaves ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ (5 : ℝ) / Real.log (↑P : ℝ), with hsum : ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ (↑k : ℝ) * ((1 : ℝ) / (↑P : ℝ)).

    Uses library nsmul_eq_mul.

    Lean, lines 73–78
      have hsum : ∑ p ∈ a.primeFactors, (1 : ℝ) / p ≤ k * (1 / P) := by
    have := Finset.sum_le_card_nsmul a.primeFactors (fun p : ℕ => (1 : ℝ) / p) (1 / P)
      (fun p hp => by
        have hp' : (P : ℝ) ≤ p := by exact_mod_cast (hbig p hp).le
        exact one_div_le_one_div_of_le hPpos hp')
    simpa [hk, nsmul_eq_mul] using this

    targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 73–78 at 0790c5bd2b57 ↗

    1. hsum.this have ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ a.primeFactors.card • ((1 : ℝ) / (↑P : ℝ))

      Leaves ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ (↑k : ℝ) * ((1 : ℝ) / (↑P : ℝ)), with this : ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ a.primeFactors.card • ((1 : ℝ) / (↑P : ℝ)).

      Uses library Finset.sum_le_card_nsmul, one_div_le_one_div_of_le.

      Lean, lines 74–77
          have := Finset.sum_le_card_nsmul a.primeFactors (fun p : ℕ => (1 : ℝ) / p) (1 / P)
      (fun p hp => by
        have hp' : (P : ℝ) ≤ p := by exact_mod_cast (hbig p hp).le
        exact one_div_le_one_div_of_le hPpos hp')

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 74–77 at 0790c5bd2b57 ↗

      1. hsum.this.hp' have (↑P : ℝ) ≤ (↑p : ℝ)

        Leaves (1 : ℝ) / (↑p : ℝ) ≤ (1 : ℝ) / (↑P : ℝ), with hp' : (↑P : ℝ) ≤ (↑p : ℝ).

        Lean, line 76
                have hp' : (P : ℝ) ≤ p := by exact_mod_cast (hbig p hp).le

        targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 76 at 0790c5bd2b57 ↗

  10. s10 calc ∑ p ∈ a.primeFactors, (1 : ℝ) / (↑p : ℝ) ≤ (↑k : ℝ) * ((1 : ℝ) / (↑P : ℝ))

    Closes the goal.

    Lean, line 79
      calc ∑ p ∈ a.primeFactors, (1 : ℝ) / p ≤ k * (1 / P) := hsum

    targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 79 at 0790c5bd2b57 ↗

  11. s11 calc

    Closes the goal.

    Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. , le_div_iff₀ See le_div_iff₀' for a version with multiplication on the other side. .

    Lean, lines 80–85
        _ ≤ 5 / Real.log P := by
      rw [le_div_iff₀ hlogP]
      have : (k : ℝ) * Real.log P ≤ 5 * P := hklog.trans hloga
      calc (k : ℝ) * (1 / P) * Real.log P = (k * Real.log P) / P := by ring
        _ ≤ (5 * P) / P := by gcongr
        _ = 5 := by field_simp

    targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, lines 80–85 at 0790c5bd2b57 ↗

    1. s11.this have (↑k : ℝ) * Real.log (↑P : ℝ) ≤ (5 : ℝ) * (↑P : ℝ)

      Leaves (↑k : ℝ) * ((1 : ℝ) / (↑P : ℝ)) * Real.log (↑P : ℝ) ≤ (5 : ℝ), with this : (↑k : ℝ) * Real.log (↑P : ℝ) ≤ (5 : ℝ) * (↑P : ℝ).

      Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. .

      Lean, line 82
            have : (k : ℝ) * Real.log P ≤ 5 * P := hklog.trans hloga

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 82 at 0790c5bd2b57 ↗

    2. s11.s2 calc (↑k : ℝ) * ((1 : ℝ) / (↑P : ℝ)) * Real.log (↑P : ℝ) = (↑k : ℝ) * Real.log (↑P : ℝ) / (↑P : ℝ) routine: ring

      Closes the goal.

      Uses library Real.log The real logarithm function, equal to the inverse of the exponential for x > 0, to log |x| for x < 0, and to 0 for 0. .

      Lean, line 83
            calc (k : ℝ) * (1 / P) * Real.log P = (k * Real.log P) / P := by ring

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 83 at 0790c5bd2b57 ↗

    3. s11.s3 calc

      Closes the goal.

      Lean, line 84
              _ ≤ (5 * P) / P := by gcongr

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 84 at 0790c5bd2b57 ↗

    4. s11.s4 calc routine: field_simp

      Closes the goal.

      Lean, line 85
              _ = 5 := by field_simp

      targets/erdos-69/nodes/spec-e0b917d1/Proof.lean, line 85 at 0790c5bd2b57 ↗

The proof in Lean (Proof.lean)

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

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/spec-e0b917d1/Proof.lean, sha256 3c13aa8baf79.
import Mathlib
import Nodes.«spec-e0b917d1».Context

/-! A speculative ingredient for erdos-69 (D-29): the correction mass of a rough dilation.
In the composite-dilation route to the irrationality of `∑ ω(n)/2^n` (see the annex on
`erdos-69` describing github.com/plby/lean-proofs, `ErdosProblems/Erdos69/RoughSizeBounds.lean`,
`roughDilation_reciprocal_mass_le`), dilating the sequence by `a = 1 + P# · (1 + j)` changes
the binary tail by a correction whose mean is controlled by `∑_{p ∣ a} 1/p`. Every prime factor of
`a` exceeds `P`, and `a ≤ 16^P`, so that sum is at most `5 / log P`. -/

theorem Opn.erdos_69_rough_dilation_reciprocal :
    ∀ P j : ℕ, 2 ≤ P → j ≤ P →
      ∑ p ∈ (1 + primorial P * (1 + j)).primeFactors, (1 : ℝ) / p ≤ 5 / Real.log P := by
  intro P j hP hj
  set a : ℕ := 1 + primorial P * (1 + j) with ha
  have ha0 : a ≠ 0 := by omega
  -- every prime factor of a exceeds P
  have hbig : ∀ p ∈ a.primeFactors, P < p := by
    intro p hp
    have hpp : p.Prime := Nat.prime_of_mem_primeFactors hp
    have hpd : p ∣ a := Nat.dvd_of_mem_primeFactors hp
    by_contra hle
    push Not at hle
    have hprim : p ∣ primorial P := by
      apply Finset.dvd_prod_of_mem
      rw [Finset.mem_filter, Finset.mem_range]
      exact ⟨by omega, hpp⟩
    have hpd' : p ∣ primorial P * (1 + j) + 1 := by rw [add_comm]; exact hpd
    have h1 : p ∣ 1 := (Nat.dvd_add_right (dvd_mul_of_dvd_left hprim (1 + j))).mp hpd'
    exact hpp.one_lt.ne' (Nat.dvd_one.mp h1)
  set k := a.primeFactors.card with hk
  have hPpos : (0 : ℝ) < P := by exact_mod_cast (show 0 < P by omega)
  have hlogP : 0 < Real.log P := Real.log_pos (by exact_mod_cast (show 1 < P by omega))
  -- P^k ≤ a
  have hpow : (P : ℝ) ^ k ≤ a := by
    have h1 : P ^ k ≤ ∏ p ∈ a.primeFactors, p := by
      rw [hk]
      exact Finset.pow_card_le_prod _ _ _ (fun p hp => (hbig p hp).le)
    have h2 : ∏ p ∈ a.primeFactors, p ≤ a :=
      Nat.le_of_dvd (Nat.pos_of_ne_zero ha0) (Nat.prod_primeFactors_dvd a)
    exact_mod_cast h1.trans h2
  -- a ≤ 16^P
  have ha16 : a ≤ 16 ^ P := by
    have h4 : primorial P ≤ 4 ^ P := primorial_le_four_pow P
    have h2 : P + 2 ≤ 4 ^ P := by
      have : P < 2 ^ P := Nat.lt_two_pow_self
      have : 4 ^ P = 2 ^ P * 2 ^ P := by rw [← mul_pow]; norm_num
      nlinarith [Nat.one_le_two_pow (n := P)]
    have h16 : 16 ^ P = 4 ^ P * 4 ^ P := by rw [← mul_pow]; norm_num
    have : primorial P * (1 + j) ≤ 4 ^ P * (1 + P) := Nat.mul_le_mul h4 (by omega)
    nlinarith
  -- log a ≤ 5 P
  have hloga : Real.log a ≤ 5 * P := by
    have hapos : (0 : ℝ) < a := by exact_mod_cast Nat.pos_of_ne_zero ha0
    have h16 : (a : ℝ) ≤ 16 ^ P := by exact_mod_cast ha16
    have he : (16 : ℝ) ≤ Real.exp 5 := by
      have h2 : (2 : ℝ) ≤ Real.exp 1 := by
        have := Real.add_one_le_exp (1 : ℝ); linarith
      have : Real.exp 5 = Real.exp 1 ^ 5 := by rw [← Real.exp_nat_mul]; norm_num
      rw [this]
      nlinarith [pow_le_pow_left₀ (by norm_num) h2 5]
    calc Real.log a ≤ Real.log (16 ^ P) := Real.log_le_log hapos h16
      _ = P * Real.log 16 := by rw [Real.log_pow]
      _ ≤ P * 5 := by
          apply mul_le_mul_of_nonneg_left _ hPpos.le
          rw [Real.log_le_iff_le_exp (by norm_num)]; exact he
      _ = 5 * P := by ring
  -- k log P ≤ log a
  have hklog : (k : ℝ) * Real.log P ≤ Real.log a := by
    have := Real.log_le_log (by positivity) hpow
    rwa [Real.log_pow] at this
  -- the sum is at most k / P
  have hsum : ∑ p ∈ a.primeFactors, (1 : ℝ) / p ≤ k * (1 / P) := by
    have := Finset.sum_le_card_nsmul a.primeFactors (fun p : ℕ => (1 : ℝ) / p) (1 / P)
      (fun p hp => by
        have hp' : (P : ℝ) ≤ p := by exact_mod_cast (hbig p hp).le
        exact one_div_le_one_div_of_le hPpos hp')
    simpa [hk, nsmul_eq_mul] using this
  calc ∑ p ∈ a.primeFactors, (1 : ℝ) / p ≤ k * (1 / P) := hsum
    _ ≤ 5 / Real.log P := by
      rw [le_div_iff₀ hlogP]
      have : (k : ℝ) * Real.log P ≤ 5 * P := hklog.trans hloga
      calc (k : ℝ) * (1 / P) * Real.log P = (k * Real.log P) / P := by ring
        _ ≤ (5 * P) / P := by gcongr
        _ = 5 := by field_simp

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.«spec-e0b917d1».Context

/-! A speculative ingredient for erdos-69 (D-29): the correction mass of a rough dilation.
In the composite-dilation route to the irrationality of `∑ ω(n)/2^n` (see the annex on
`erdos-69` describing github.com/plby/lean-proofs, `ErdosProblems/Erdos69/RoughSizeBounds.lean`,
`roughDilation_reciprocal_mass_le`), dilating the sequence by `a = 1 + P# · (1 + j)` changes
the binary tail by a correction whose mean is controlled by `∑_{p ∣ a} 1/p`. Every prime factor of
`a` exceeds `P`, and `a ≤ 16^P`, so that sum is at most `5 / log P`. -/

theorem Opn.erdos_69_rough_dilation_reciprocal :
    ∀ P j : ℕ, 2 ≤ P → j ≤ P →
      ∑ p ∈ (1 + primorial P * (1 + j)).primeFactors, (1 : ℝ) / p ≤ 5 / Real.log P := 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 P,j\in\mathbb{N},\ 2\le P,\ j\le P:\quad \sum_{p\mid 1+P\#\,(1+j)}\frac{1}{p} \le \frac{5}{\log P}$

For naturals P ≥ 2 and j ≤ P, the sum of 1/p over the prime factors p of 1 + P#·(1+j) is at most 5/log P, where P# is the primorial (the product of the primes at most P), the sum runs over (…).primeFactors, and log is the natural logarithm, all in ℝ.

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

Rendered from targets/erdos-69/nodes/spec-e0b917d1/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000310.json, merge commit 0790c5bd2b57.

Verdict pass, from attestations/000310.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/000310.json, merge commit 0790c5bd2b57.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-69/nodes/spec-e0b917d1/Witness.lean, sha256 41d59df8631c.
import Mathlib

theorem witness : ∃ P j : ℕ, 2 ≤ P ∧ j ≤ P := ⟨2, 0, le_rfl, Nat.zero_le _⟩

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 (3)

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

Untrusted: acknowledgment of a div-zero finding at 1 / ↑p

p ranges over the prime factors of a positive integer, so p ≥ 2 and 1/p is never the junk value.

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

Untrusted: acknowledgment of a div-zero finding at 5 / Real.log ↑P

The hypothesis 2 ≤ P makes log P positive, so the divisor is never 0.

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

Untrusted: acknowledgment of a off-by-one-range finding at 2 ≤ P

Inclusive on purpose: the bound is claimed for every P ≥ 2; at P = 1 the right side would divide by log 1 = 0.

How to read this page

How to read a statement’s page →