purely periodic sets (Luca–Tachiya)

Untrusted contributor text — a partial assembly: it records an attempt, not a proof; its attestation names the file, and no hash in the record binds these bytes.

Untrusted: partial assembly (D-12 #5), by t1026-b; merged in 67f814cc5251 under attestations/000981.json, whose step 2 took this file as a partial. A partial records an attempt, not a proof: the gate replayed it with its holes left as sorry. Rendered from targets/erdos-257/nodes/variant-5274cf38--h1/attempts/20261026T205203Z-t1026-b-partial.lean.

import Mathlib
import Nodes.«variant-5274cf38--h1».Context

/-! Hole `hper` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

/- The divisor-counting function. -/
private def dd (n : ℕ) : ℕ := n.divisors.card

/- `f_B(n)`: the number of divisors of `n` that lie in `B`. -/
private def fB (B : Set ℕ) [DecidablePred (· ∈ B)] (n : ℕ) : ℕ :=
  (n.divisors.filter (· ∈ B)).card

private lemma fB_eq_ncard (B : Set ℕ) [DecidablePred (· ∈ B)] (n : ℕ) :
    fB B n = Set.ncard {d : ℕ | d ∈ n.divisors ∧ d ∈ B} := by
  unfold fB
  rw [← Set.ncard_coe_finset]
  congr 1
  ext d
  simp

private lemma fB_le_dd (B : Set ℕ) [DecidablePred (· ∈ B)] (n : ℕ) : fB B n ≤ dd n :=
  Finset.card_filter_le _ _

private lemma fB_le (B : Set ℕ) [DecidablePred (· ∈ B)] (n : ℕ) : fB B n ≤ n :=
  (fB_le_dd B n).trans (Nat.card_divisors_le_self n)

private lemma fB_pos (B : Set ℕ) [DecidablePred (· ∈ B)] {n : ℕ} (hn : n ≠ 0) (hnB : n ∈ B) :
    0 < fB B n := by
  unfold fB
  exact Finset.card_pos.mpr ⟨n, by simp [Finset.mem_filter, Nat.mem_divisors, hn, hnB]⟩

/- A periodic set has an element beyond every `j`. -/
private lemma exists_mem_gt {B : Set ℕ} {P : ℕ} (hP : 0 < P)
    (hper : ∀ n, n ∈ B ↔ n + P ∈ B) {r : ℕ} (hr : r ∈ B) (j : ℕ) : ∃ i, j + i + 1 ∈ B := by
  have hiter : ∀ k, r + P * k ∈ B := by
    intro k
    induction k with
    | zero => simpa using hr
    | succ k ih =>
      rw [show r + P * (k + 1) = (r + P * k) + P by ring]
      exact (hper _).1 ih
  refine ⟨r + P * (j + 1) - j - 1, ?_⟩
  have : j + 1 ≤ r + P * (j + 1) := by nlinarith
  rw [show j + (r + P * (j + 1) - j - 1) + 1 = r + P * (j + 1) by omega]
  exact hiter _

/- `b` times the "tail" `∑_{i ≥ 1} f(j+i) / 2^i`. -/
private noncomputable def Tail (f : ℕ → ℕ) (b : ℕ) (j : ℕ) : ℝ :=
  b * ∑' i : ℕ, (f (j + i + 1) : ℝ) / 2 ^ (i + 1)

/- The integer that the tail equals when the series is `a / b`. -/
private def Zint (f : ℕ → ℕ) (a : ℤ) (b : ℕ) (j : ℕ) : ℤ :=
  a * 2 ^ j - b * ∑ n ∈ Finset.range (j + 1), (f n : ℤ) * 2 ^ (j - n)

private lemma summable_shift {f : ℕ → ℕ} (hf : ∀ n, f n ≤ n) (j : ℕ) :
    Summable (fun i : ℕ => (f (j + i + 1) : ℝ) / 2 ^ (i + 1)) := by
  have h : Summable (fun i : ℕ => ((j + 1 : ℝ) + i) * (1/2) ^ i) := by
    have h1 := (summable_geometric_two).mul_left (j+1 : ℝ)
    have h2 := summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
      (by norm_num [abs_of_pos])
    simpa [add_mul] using h1.add h2
  refine Summable.of_nonneg_of_le (fun i => by positivity) (fun i => ?_) h
  have : (f (j + i + 1) : ℝ) ≤ j + i + 1 := by exact_mod_cast hf _
  rw [div_eq_mul_inv, pow_succ, mul_inv, one_div, inv_pow]
  have : (0:ℝ) ≤ (2 ^ i)⁻¹ := by positivity
  nlinarith

private lemma summable_f {f : ℕ → ℕ} (hf : ∀ n, f n ≤ n) :
    Summable (fun n : ℕ => (f n : ℝ) / 2 ^ n) := by
  have h2 := summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
    (by norm_num [abs_of_pos])
  refine Summable.of_nonneg_of_le (fun i => by positivity) (fun i => ?_) h2
  have : (f i : ℝ) ≤ i := by exact_mod_cast hf _
  rw [div_eq_mul_inv, one_div, inv_pow, pow_one]
  have : (0:ℝ) ≤ (2 ^ i)⁻¹ := by positivity
  nlinarith

private lemma tail_pos {f : ℕ → ℕ} (hf : ∀ n, f n ≤ n) {b : ℕ} (hb : 0 < b) (j : ℕ)
    {i₀ : ℕ} (hi₀ : 0 < f (j + i₀ + 1)) : 0 < Tail f b j := by
  unfold Tail
  apply mul_pos (by exact_mod_cast hb)
  apply (summable_shift hf j).tsum_pos (fun i => by positivity) i₀
  positivity

private lemma tail_upper {f : ℕ → ℕ} (hf : ∀ n, f n ≤ n) (b j L : ℕ) :
    Tail f b j ≤ b * ∑ i ∈ Finset.range L, (f (j + i + 1) : ℝ) / 2 ^ (i + 1)
      + b * ((j + L + 2 : ℝ) / 2 ^ L) := by
  unfold Tail
  rw [← (summable_shift hf j).sum_add_tsum_nat_add L, mul_add]
  gcongr
  have hg1 : Summable (fun i : ℕ => (1/2 : ℝ) ^ i) := summable_geometric_two
  have hg2 : Summable (fun i : ℕ => (i : ℝ) * (1/2 : ℝ) ^ i) := by
    simpa using summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
      (by norm_num [abs_of_pos])
  have key : ∑' i : ℕ, ((j + L + 1 : ℝ) / 2 ^ (L + 1) * (1/2) ^ i
      + 1 / 2 ^ (L + 1) * ((i : ℝ) * (1/2) ^ i)) = (j + L + 2 : ℝ) / 2 ^ L := by
    rw [(hg1.mul_left _).tsum_add (hg2.mul_left _), tsum_mul_left, tsum_mul_left,
      tsum_geometric_two, tsum_coe_mul_geometric_of_norm_lt_one (by norm_num [abs_of_pos])]
    rw [pow_succ]; field_simp; ring
  rw [← key]
  refine Summable.tsum_le_tsum (fun i => ?_) ((summable_nat_add_iff L).mpr (summable_shift hf j))
    ((hg1.mul_left _).add (hg2.mul_left _))
  have : (f (j + (i + L) + 1) : ℝ) ≤ j + L + 1 + i := by
    have := hf (j + (i + L) + 1)
    have : (f (j + (i + L) + 1) : ℝ) ≤ ((j + (i + L) + 1 : ℕ) : ℝ) := by exact_mod_cast this
    push_cast at this; linarith
  show (f (j + (i + L) + 1) : ℝ) / 2 ^ (i + L + 1) ≤ _
  rw [show (2:ℝ) ^ (i + L + 1) = 2 ^ (L+1) * 2 ^ i by ring, one_div_pow]
  rw [div_le_iff₀ (by positivity)]
  field_simp
  linarith

private lemma tail_eq_Zint {f : ℕ → ℕ} (hf : ∀ n, f n ≤ n) {a : ℤ} {b : ℕ} (hb : 0 < b)
    (h : ∑' n : ℕ, (f n : ℝ) / 2 ^ n = a / b) (j : ℕ) : Tail f b j = Zint f a b j := by
  have hsplit := (summable_f hf).sum_add_tsum_nat_add (j + 1)
  have htail : ∑' i : ℕ, (f (i + (j + 1)) : ℝ) / 2 ^ (i + (j + 1)) =
      (1 / 2 ^ j) * ∑' i : ℕ, (f (j + i + 1) : ℝ) / 2 ^ (i + 1) := by
    rw [← tsum_mul_left]
    apply tsum_congr; intro i
    rw [show i + (j + 1) = j + i + 1 by ring,
      show (2:ℝ) ^ (j + i + 1) = 2 ^ j * 2 ^ (i + 1) by ring]
    field_simp
  rw [htail, h] at hsplit
  have hb' : (b : ℝ) ≠ 0 := by exact_mod_cast hb.ne'
  have hT : Tail f b j = 2 ^ j * (a - b * ∑ n ∈ Finset.range (j + 1), (f n : ℝ) / 2 ^ n) := by
    unfold Tail
    field_simp at hsplit
    have : (2:ℝ) ^ j ≠ 0 := by positivity
    field_simp
    linear_combination hsplit
  rw [hT]
  unfold Zint
  push_cast
  rw [mul_sub, Finset.mul_sum, Finset.mul_sum, Finset.mul_sum]
  congr 1
  · ring
  · apply Finset.sum_congr rfl; intro n hn
    have hn' : n ≤ j := Nat.lt_succ_iff.mp (Finset.mem_range.mp hn)
    rw [pow_sub₀ _ (by norm_num) hn']
    field_simp

private lemma Zint_dvd (f : ℕ → ℕ) (a : ℤ) (b k m : ℕ)
    (hd : ∀ n, k < n → n ≤ k + m → 2 ^ m ∣ f n) :
    (2 : ℤ) ^ m ∣ Zint f a b (k + m) := by
  unfold Zint
  apply dvd_sub
  · exact Dvd.dvd.mul_left (pow_dvd_pow 2 (by omega)) _
  · apply Dvd.dvd.mul_left
    apply Finset.dvd_sum
    intro n hn
    have hn' : n ≤ k + m := Nat.lt_succ_iff.mp (Finset.mem_range.mp hn)
    by_cases hnk : n ≤ k
    · exact Dvd.dvd.mul_left (pow_dvd_pow 2 (by omega)) _
    · apply Dvd.dvd.mul_right
      exact_mod_cast hd n (by omega) hn'

private lemma dd_le_two_mul_small (n : ℕ) :
    dd n ≤ 2 * (n.divisors.filter (fun e => e * e ≤ n)).card := by
  unfold dd
  rw [← Finset.card_filter_add_card_filter_not (fun e => e * e ≤ n)]
  have : (n.divisors.filter (fun e => ¬ e * e ≤ n)).card ≤
      (n.divisors.filter (fun e => e * e ≤ n)).card := by
    apply Finset.card_le_card_of_injOn (fun e => n / e)
    · intro e he
      simp only [Finset.coe_filter, Nat.mem_divisors, not_le, Set.mem_setOf_eq] at he ⊢
      obtain ⟨⟨hd, hn⟩, hlt⟩ := he
      have hepos : 0 < e := Nat.pos_of_dvd_of_pos hd (Nat.pos_of_ne_zero hn)
      refine ⟨⟨Nat.div_dvd_of_dvd hd, hn⟩, ?_⟩
      have h1 : n / e < e := (Nat.div_lt_iff_lt_mul hepos).mpr hlt
      calc n / e * (n / e) ≤ n / e * e := Nat.mul_le_mul_left _ h1.le
        _ = n := Nat.div_mul_cancel hd
    · intro e1 h1 e2 h2 h
      simp only [Finset.coe_filter, Nat.mem_divisors, Set.mem_setOf_eq] at h1 h2
      have := congrArg (fun x => n / x) h
      simp only at this
      rwa [Nat.div_div_self h1.1.1 h1.1.2, Nat.div_div_self h2.1.1 h2.1.2] at this
  omega

private lemma card_AP_dvd_le (r Q X e : ℕ) (hcop : Nat.Coprime r Q) :
    ((Finset.range X).filter (fun t => (e + 1) ∣ r + t * Q)).card ≤ X / (e + 1) + 1 := by
  set E := e + 1 with hE
  have hEpos : 0 < E := by omega
  have key : ∀ t1 ∈ (Finset.range X).filter (fun t => E ∣ r + t * Q),
      ∀ t2 ∈ (Finset.range X).filter (fun t => E ∣ r + t * Q), t1 / E = t2 / E → t1 ≤ t2 → t1 = t2 := by
    intro t1 h1 t2 h2 hq hle
    simp only [Finset.mem_filter, Finset.mem_range] at h1 h2
    have hcopE : Nat.Coprime E Q := by
      have hg1 : Nat.gcd E Q ∣ r + t1 * Q := (Nat.gcd_dvd_left E Q).trans h1.2
      have hg2 : Nat.gcd E Q ∣ t1 * Q := Dvd.dvd.mul_left (Nat.gcd_dvd_right E Q) _
      have hg3 : Nat.gcd E Q ∣ r := (Nat.dvd_add_left hg2).mp hg1
      have hg4 : Nat.gcd E Q ∣ Nat.gcd r Q := Nat.dvd_gcd hg3 (Nat.gcd_dvd_right E Q)
      rw [hcop] at hg4
      exact Nat.dvd_one.mp hg4
    have hd : E ∣ (t2 - t1) * Q := by
      have := Nat.dvd_sub h2.2 h1.2
      rwa [show r + t2 * Q - (r + t1 * Q) = (t2 - t1) * Q by rw [Nat.sub_mul]; omega] at this
    have hd2 : E ∣ t2 - t1 := hcopE.dvd_of_dvd_mul_right hd
    have hlt : t2 - t1 < E := by
      have e1 := Nat.div_add_mod t1 E
      have e2 := Nat.div_add_mod t2 E
      have m1 := Nat.mod_lt t1 hEpos
      have m2 := Nat.mod_lt t2 hEpos
      rw [hq] at e1
      omega
    have := Nat.eq_zero_of_dvd_of_lt hd2 hlt
    omega
  calc ((Finset.range X).filter (fun t => E ∣ r + t * Q)).card ≤ (Finset.range (X / E + 1)).card := by
        apply Finset.card_le_card_of_injOn (fun t => t / E)
        · intro t ht
          simp only [Finset.coe_filter, Finset.mem_range, Set.mem_setOf_eq] at ht
          simp only [Finset.coe_range, Set.mem_Iio]
          have := Nat.div_le_div_right (c := E) ht.1.le
          omega
        · intro t1 h1 t2 h2 hq
          rcases le_total t1 t2 with h | h
          · exact key t1 h1 t2 h2 hq h
          · exact (key t2 h2 t1 h1 hq.symm h).symm
    _ = X / E + 1 := Finset.card_range _

private lemma sum_dd_AP_le (r Q X : ℕ) (hcop : Nat.Coprime r Q)
    (hX : ∀ t < X, r + t * Q ≤ X * X) :
    (∑ t ∈ Finset.range X, (dd (r + t * Q) : ℝ)) ≤ 2 * X * (2 + Real.log X) := by
  have hnat : ∑ t ∈ Finset.range X, dd (r + t * Q) ≤ 2 * ∑ e ∈ Finset.range X, (X / (e + 1) + 1) := by
    calc ∑ t ∈ Finset.range X, dd (r + t * Q)
        ≤ ∑ t ∈ Finset.range X, 2 * ((Finset.range X).filter (fun e => (e + 1) ∣ r + t * Q)).card := by
          apply Finset.sum_le_sum; intro t ht
          refine (dd_le_two_mul_small _).trans ?_
          apply Nat.mul_le_mul_left
          apply Finset.card_le_card_of_injOn (fun e => e - 1)
          · intro e he
            simp only [Finset.coe_filter, Nat.mem_divisors, Set.mem_setOf_eq] at he
            simp only [Finset.coe_filter, Finset.mem_range, Set.mem_setOf_eq]
            have hepos : 0 < e := Nat.pos_of_dvd_of_pos he.1.1 (Nat.pos_of_ne_zero he.1.2)
            have : e * e ≤ X * X := he.2.trans (hX t (by simpa using ht))
            have : e ≤ X := Nat.mul_self_le_mul_self_iff.mp this
            refine ⟨by omega, ?_⟩
            rw [Nat.sub_add_cancel hepos]; exact he.1.1
          · intro e1 h1 e2 h2 h
            simp only [Finset.coe_filter, Nat.mem_divisors, Set.mem_setOf_eq] at h1 h2
            have := Nat.pos_of_dvd_of_pos h1.1.1 (Nat.pos_of_ne_zero h1.1.2)
            have := Nat.pos_of_dvd_of_pos h2.1.1 (Nat.pos_of_ne_zero h2.1.2)
            simp only at h
            omega
      _ = 2 * ∑ e ∈ Finset.range X, ((Finset.range X).filter (fun t => (e + 1) ∣ r + t * Q)).card := by
          rw [← Finset.mul_sum]
          congr 1
          simp only [Finset.card_filter]
          exact Finset.sum_comm
      _ ≤ 2 * ∑ e ∈ Finset.range X, (X / (e + 1) + 1) := by
          apply Nat.mul_le_mul_left
          exact Finset.sum_le_sum fun e _ => card_AP_dvd_le r Q X e hcop
  have hreal : ((∑ e ∈ Finset.range X, (X / (e + 1) + 1) : ℕ) : ℝ) ≤ X * (1 + Real.log X) + X := by
    push_cast
    rw [Finset.sum_add_distrib]
    simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_one]
    gcongr
    calc ∑ e ∈ Finset.range X, ((X / (e + 1) : ℕ) : ℝ) ≤ ∑ e ∈ Finset.range X, (X : ℝ) / (e + 1) := by
          apply Finset.sum_le_sum; intro e _
          have := Nat.cast_div_le (α := ℝ) (m := X) (n := e + 1)
          push_cast at this; exact this
      _ = X * (harmonic X : ℝ) := by
          rw [harmonic]; push_cast; rw [Finset.mul_sum]
          apply Finset.sum_congr rfl; intro e _; field_simp
      _ ≤ X * (1 + Real.log X) := by
          gcongr
          exact harmonic_le_one_add_log X
  have h1 : (∑ t ∈ Finset.range X, (dd (r + t * Q) : ℝ)) ≤
      2 * ((∑ e ∈ Finset.range X, (X / (e + 1) + 1) : ℕ) : ℝ) := by
    exact_mod_cast hnat
  linarith

private lemma exists_param (b m₀ : ℕ) :
    ∃ m : ℕ, b ≤ m ∧ m₀ ≤ m ∧ 1 ≤ m ∧ 15 * m ^ 5 < 2 ^ m := by
  have h := tendsto_pow_const_div_const_pow_of_one_lt 5 (r := (2:ℝ)) (by norm_num)
  have h2 := (h.eventually (gt_mem_nhds (show (0:ℝ) < 1/15 by norm_num))).and
    (Filter.eventually_ge_atTop (max b (max m₀ 1)))
  obtain ⟨m, hm, hmb⟩ := h2.exists
  refine ⟨m, le_of_max_le_left hmb, le_of_max_le_left (le_of_max_le_right hmb),
    le_of_max_le_right (le_of_max_le_right hmb), ?_⟩
  have : (m : ℝ) ^ 5 < 1 / 15 * 2 ^ m := by
    rwa [div_lt_iff₀ (by positivity)] at hm
  have : (15 * m ^ 5 : ℝ) < 2 ^ m := by linarith
  exact_mod_cast this

private lemma idx_inj {m i j i' j' : ℕ} (hj : j < m) (hj' : j' < m) (h : i * m + j = i' * m + j') :
    i = i' ∧ j = j' := by
  rcases lt_trichotomy i i' with hi | hi | hi
  · exfalso
    have : (i + 1) * m ≤ i' * m := Nat.mul_le_mul_right _ hi
    nlinarith
  · subst hi; omega
  · exfalso
    have : (i' + 1) * m ≤ i * m := Nat.mul_le_mul_right _ hi
    nlinarith

/- Numerical facts about the parameters. -/
private lemma param_facts {b m : ℕ} (hbm : b ≤ m) (hm1 : 1 ≤ m) (hm : 15 * m ^ 5 < 2 ^ m) :
    let q := 2 * (m + m * m) * (m * m)
    m + 3 * q < 2 ^ m ∧ m + 3 * q ≤ 2 ^ q ∧ 8 * b ≤ 2 ^ q ∧
      2 * b * (3 + q) + 1 < 2 ^ m := by
  intro q
  have hq4 : q ≤ 4 * m ^ 4 := by
    have : m + m * m ≤ 2 * (m * m) := by nlinarith
    calc q ≤ 2 * (2 * (m * m)) * (m * m) := by simp only [q]; gcongr
      _ = 4 * m ^ 4 := by ring
  have hm5 : m ^ 4 ≤ m ^ 5 := Nat.pow_le_pow_right hm1 (by norm_num)
  have hm5' : m ≤ m ^ 5 := by
    calc m = m ^ 1 := (pow_one m).symm
      _ ≤ m ^ 5 := Nat.pow_le_pow_right hm1 (by norm_num)
  have hmq : m ≤ q := by
    simp only [q]; nlinarith
  have h2q : 2 ^ m ≤ 2 ^ q := Nat.pow_le_pow_right (by norm_num) hmq
  refine ⟨by omega, by omega, by omega, ?_⟩
  have : b * (3 + q) ≤ m * (3 + 4 * m ^ 4) := Nat.mul_le_mul hbm (by omega)
  have : m * (3 + 4 * m ^ 4) = 3 * m + 4 * m ^ 5 := by ring
  have : 2 * b * (3 + q) = 2 * (b * (3 + q)) := by ring
  omega

private lemma mem_iff_add_mul {B : Set ℕ} {P : ℕ} (hper : ∀ n, n ∈ B ↔ n + P ∈ B) (n k : ℕ) :
    n ∈ B ↔ n + P * k ∈ B := by
  induction k with
  | zero => simp
  | succ k ih =>
    rw [ih, hper (n + P * k), show n + P * k + P = n + P * (k + 1) by ring]

/- A prime `p ≡ 1 (mod P)` not dividing `r` doubles `f_B`: the divisors of `p r` are the
divisors `d` of `r` and the numbers `p d`, and `p d ≡ d (mod P)`. -/
private lemma fB_mul_prime (B : Set ℕ) [DecidablePred (· ∈ B)] {P : ℕ} (hP : 0 < P)
    (hper : ∀ n, n ∈ B ↔ n + P ∈ B) {p r : ℕ} (hp : p.Prime) (hpP : p % P = 1)
    (hpr : ¬ p ∣ r) (hr : r ≠ 0) : fB B (p * r) = 2 * fB B r := by
  have hpd : ∀ d, p * d = d + P * (p / P * d) := by
    intro d
    have := Nat.div_add_mod p P
    rw [hpP] at this
    calc p * d = (P * (p / P) + 1) * d := by rw [this]
      _ = d + P * (p / P * d) := by ring
  have hpB : ∀ d, p * d ∈ B ↔ d ∈ B := by
    intro d
    rw [hpd d]
    exact (mem_iff_add_mul hper d _).symm
  have hpr0 : p * r ≠ 0 := mul_ne_zero hp.ne_zero hr
  have hsplit : (p * r).divisors.filter (· ∈ B) =
      (r.divisors.filter (· ∈ B)) ∪
        ((r.divisors.filter (· ∈ B)).map ⟨(p * ·), mul_right_injective₀ hp.ne_zero⟩) := by
    ext D
    simp only [Finset.mem_filter, Nat.mem_divisors, Finset.mem_union, Finset.mem_map,
      Function.Embedding.coeFn_mk]
    constructor
    · rintro ⟨⟨hD, -⟩, hDB⟩
      by_cases hpD : p ∣ D
      · obtain ⟨d, rfl⟩ := hpD
        right
        refine ⟨d, ⟨⟨?_, hr⟩, (hpB d).1 hDB⟩, rfl⟩
        exact (Nat.mul_dvd_mul_iff_left hp.pos).1 hD
      · left
        refine ⟨⟨?_, hr⟩, hDB⟩
        exact Nat.Coprime.dvd_of_dvd_mul_left ((Nat.Prime.coprime_iff_not_dvd hp).2 hpD).symm hD
    · rintro (⟨⟨hD, -⟩, hDB⟩ | ⟨d, ⟨⟨hd, -⟩, hdB⟩, rfl⟩)
      · exact ⟨⟨dvd_mul_of_dvd_right hD p, hpr0⟩, hDB⟩
      · exact ⟨⟨mul_dvd_mul_left p hd, hpr0⟩, (hpB d).2 hdB⟩
  have hdisj : Disjoint (r.divisors.filter (· ∈ B))
      ((r.divisors.filter (· ∈ B)).map ⟨(p * ·), mul_right_injective₀ hp.ne_zero⟩) := by
    rw [Finset.disjoint_left]
    intro D hD hD'
    simp only [Finset.mem_filter, Nat.mem_divisors, Finset.mem_map,
      Function.Embedding.coeFn_mk] at hD hD'
    obtain ⟨d, -, rfl⟩ := hD'
    exact hpr (dvd_trans (dvd_mul_right p d) hD.1.1)
  unfold fB
  rw [hsplit, Finset.card_union_of_disjoint hdisj, Finset.card_map]
  ring

/- Each of `S`'s primes, `≡ 1 (mod P)` and dividing `n` exactly once, doubles `f_B`. -/
private lemma pow_two_dvd_fB (B : Set ℕ) [DecidablePred (· ∈ B)] {P : ℕ} (hP : 0 < P)
    (hper : ∀ n, n ∈ B ↔ n + P ∈ B) (S : Finset ℕ) : ∀ n : ℕ, n ≠ 0 →
    (∀ p ∈ S, p.Prime ∧ p % P = 1 ∧ p ∣ n ∧ ¬ p ^ 2 ∣ n) → 2 ^ S.card ∣ fB B n := by
  refine Finset.induction_on S ?_ ?_
  · intro n _ _
    simp
  · intro p S hpS ih n hn hS
    obtain ⟨hp, hpP, hpn, hp2⟩ := hS p (Finset.mem_insert_self _ _)
    obtain ⟨r, rfl⟩ := hpn
    have hr : r ≠ 0 := by
      rintro rfl
      simp at hn
    have hpr : ¬ p ∣ r := fun h => hp2 (by rw [pow_two]; exact mul_dvd_mul_left p h)
    rw [Finset.card_insert_of_notMem hpS, pow_succ, fB_mul_prime B hP hper hp hpP hpr hr,
      mul_comm (2 ^ S.card) 2]
    apply mul_dvd_mul_left 2
    apply ih r hr
    intro q hq
    obtain ⟨hqpr, hqP, hqn, hq2⟩ := hS q (Finset.mem_insert_of_mem hq)
    have hqp : q ≠ p := fun h => hpS (h ▸ hq)
    refine ⟨hqpr, hqP, ?_, ?_⟩
    · exact Nat.Coprime.dvd_of_dvd_mul_left ((Nat.coprime_primes hqpr hp).2 hqp) hqn
    · intro h
      exact hq2 (dvd_mul_of_dvd_right h p)

private lemma tsum_pnat_of_zero (f : ℕ → ℝ) (h0 : f 0 = 0) : ∑' n : ℕ+, f n = ∑' n : ℕ, f n := by
  apply Function.Injective.tsum_eq PNat.coe_injective
  intro n hn
  have : n ≠ 0 := by rintro rfl; exact hn h0
  exact ⟨⟨n, Nat.pos_of_ne_zero this⟩, rfl⟩

private lemma geom_pnat {x : ℝ} (hx : |x| < 1) : ∑' c : ℕ+, x ^ (c : ℕ) = x / (1 - x) := by
  rw [tsum_pnat_eq_tsum_succ (f := fun m : ℕ => x ^ m)]
  simp_rw [pow_succ]
  rw [tsum_mul_right, tsum_geometric_of_abs_lt_one hx]
  ring

/- The Lambert identity for a set: `∑_{n ∈ B} 1/(2^n - 1) = ∑_m f_B(m) / 2^m`. -/
private lemma lambert_set (B : Set ℕ) [DecidablePred (· ∈ B)] :
    ∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ))
      = ∑' m : ℕ, (fB B m : ℝ) / 2 ^ m := by
  set w : ℕ → ℝ := fun d => if d ∈ B then 1 else 0 with hw
  have hw01 : ∀ d, 0 ≤ w d ∧ w d ≤ 1 := fun d => by
    simp only [hw]; split_ifs <;> norm_num
  set r : ℝ := 1 / 2 with hr
  have hr1 : ‖r‖ < 1 := by rw [hr, Real.norm_eq_abs, abs_of_pos (by norm_num)]; norm_num
  set G : ℕ+ × ℕ+ → ℝ := fun c => w c.1 * r ^ ((c.1 : ℕ) * (c.2 : ℕ)) with hG
  have hGs : Summable G := by
    have h := summable_prod_mul_pow (𝕜 := ℝ) 0 hr1
    refine Summable.of_nonneg_of_le (fun c => ?_) (fun c => ?_) h
    · exact mul_nonneg (hw01 _).1 (by positivity)
    · simp only [pow_zero, one_mul]
      exact mul_le_of_le_one_left (by positivity) (hw01 _).2
  have hprod : ∑' c : ℕ+ × ℕ+, G c = ∑' d : ℕ+, w d / (2 ^ (d : ℕ) - 1) := by
    rw [hGs.tsum_prod]
    refine tsum_congr fun d => ?_
    simp only [hG]
    simp_rw [pow_mul]
    rw [tsum_mul_left, geom_pnat ?_]
    · have h3 : (2:ℝ) ^ (d:ℕ) - 1 ≠ 0 := by
        have : (1:ℝ) < 2 ^ (d:ℕ) := one_lt_pow₀ (by norm_num) d.ne_zero
        linarith
      rw [hr, one_div_pow]
      field_simp
    · rw [hr, one_div_pow, abs_of_pos (by positivity), div_lt_one (by positivity)]
      exact one_lt_pow₀ (by norm_num) d.ne_zero
  have hsig : ∑' c : ℕ+ × ℕ+, G c = ∑' e : ℕ+, (fB B e : ℝ) * r ^ (e : ℕ) := by
    rw [← sigmaAntidiagonalEquivProd.tsum_eq]
    have hs : Summable (fun x => G (sigmaAntidiagonalEquivProd x)) :=
      (Equiv.summable_iff _).2 hGs
    rw [hs.tsum_sigma]
    refine tsum_congr fun e => ?_
    rw [tsum_fintype]
    simp only [sigmaAntidiagonalEquivProd, divisorsAntidiagonalFactors, Equiv.coe_fn_mk,
      PNat.mk_coe, hG]
    rw [Finset.univ_eq_attach,
      (e : ℕ).divisorsAntidiagonal.sum_attach (fun x : ℕ × ℕ => w x.1 * r ^ (x.1 * x.2)),
      Nat.sum_divisorsAntidiagonal (fun a b => w a * r ^ (a * b))]
    rw [Finset.sum_congr rfl (fun a ha => by
      rw [Nat.mul_div_cancel' (Nat.dvd_of_mem_divisors ha)] :
        ∀ a ∈ (e : ℕ).divisors, w a * r ^ (a * ((e : ℕ) / a)) = w a * r ^ (e : ℕ))]
    rw [← Finset.sum_mul]
    congr 1
    unfold fB
    rw [Finset.card_filter]
    push_cast
    rfl
  have hL : ∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ))
      = ∑' d : ℕ+, w d / (2 ^ (d : ℕ) - 1) := by
    rw [tsum_subtype B (fun n : ℕ => (1 : ℝ) / ((2:ℝ) ^ n - 1))]
    rw [tsum_pnat_of_zero (fun n : ℕ => w n / (2 ^ n - 1)) (by simp)]
    refine tsum_congr fun n => ?_
    simp only [Set.indicator_apply, hw]
    split_ifs <;> simp
  have hR : ∑' m : ℕ, (fB B m : ℝ) / 2 ^ m = ∑' e : ℕ+, (fB B e : ℝ) * r ^ (e : ℕ) := by
    rw [← tsum_pnat_of_zero (fun m : ℕ => (fB B m : ℝ) / 2 ^ m) (by simp [fB])]
    refine tsum_congr fun e => ?_
    rw [hr, one_div_pow, div_eq_mul_inv, one_div]
  rw [hL, hR, ← hprod, ← hsig]

/- The averaging contradiction: the lower bounds `2^m ≤ Tail` along an arithmetic progression
are incompatible with the average size of the divisor function, which dominates `f`. -/
private lemma averaging_contra {f : ℕ → ℕ} (hfdd : ∀ n, f n ≤ dd n)
    {b m q Q c : ℕ} (hb : 0 < b) (hQpos : 0 < Q) (hcQ : c < Q)
    (hQle : Q ≤ 2 ^ q) (hA2 : m + 3 * q ≤ 2 ^ q) (hA3 : 8 * b ≤ 2 ^ q)
    (hA4 : 2 * b * (3 + q) + 1 < 2 ^ m)
    (hcop : ∀ i < 3 * q, Nat.Coprime (c + m + i + 1) Q)
    (hlow : ∀ t, (2 : ℝ) ^ m ≤ Tail f b (c + t * Q + m)) : False := by
  have hf : ∀ n, f n ≤ n := fun n => (hfdd n).trans (Nat.card_divisors_le_self n)
  set L := 3 * q with hLdef
  set X := Q + m + L with hXdef
  -- numerical facts
  have hX1 : 1 ≤ X := by omega
  have hXpow : X ≤ 2 ^ (q + 1) := by rw [pow_succ]; omega
  have hLX : 2 * b * X ^ 2 ≤ 2 ^ L := by
    calc 2 * b * X ^ 2 ≤ 2 * b * (2 ^ (q + 1)) ^ 2 := by gcongr
      _ = 8 * b * (2 ^ q * 2 ^ q) := by ring
      _ ≤ 2 ^ q * (2 ^ q * 2 ^ q) := by gcongr
      _ = 2 ^ L := by rw [hLdef]; ring
  have hrange : ∀ t < X, c + t * Q < X * Q := by
    intro t ht
    have : (t + 1) * Q ≤ X * Q := Nat.mul_le_mul_right _ ht
    nlinarith
  have hXX : X * Q + m + L ≤ X * X := by
    have : X * X = X * Q + X * (m + L) := by rw [hXdef]; ring
    have : m + L ≤ X * (m + L) := Nat.le_mul_of_pos_left _ hX1
    omega
  -- upper bound for each t
  have hupt : ∀ t < X, Tail f b (c + t * Q + m) ≤
      b * ∑ i ∈ Finset.range L, (f (c + m + i + 1 + t * Q) : ℝ) / 2 ^ (i + 1)
        + b * ((2 * X ^ 2 : ℕ) / 2 ^ L : ℝ) := by
    intro t ht
    have h := tail_upper hf b (c + t * Q + m) L
    have e : ∀ i, c + t * Q + m + i + 1 = c + m + i + 1 + t * Q := fun i => by ring
    simp only [e] at h
    refine h.trans (add_le_add le_rfl ?_)
    gcongr
    have := hrange t ht
    have h2 : c + t * Q + m + L + 2 ≤ 2 * X ^ 2 := by nlinarith
    exact_mod_cast h2
  have hgeom : ∀ L : ℕ, ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1) ≤ 1 := by
    intro L
    have : ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1) = 1 - (1 / 2) ^ L := by
      induction L with
      | zero => simp
      | succ n ih => rw [Finset.sum_range_succ, ih]; ring
    rw [this]; linarith [pow_pos (by norm_num : (0 : ℝ) < 1 / 2) L]
  set B : ℝ := 2 * X * (2 + Real.log X) with hBdef
  have hF : ∀ i ∈ Finset.range L, (∑ t ∈ Finset.range X, (f (c + m + i + 1 + t * Q) : ℝ)) ≤ B := by
    intro i hi
    refine le_trans (Finset.sum_le_sum fun t _ => ?_)
      (sum_dd_AP_le _ _ _ (hcop i (by simpa using hi)) ?_)
    · exact_mod_cast hfdd _
    · intro t ht
      have := hrange t ht
      have : i < L := by simpa using hi
      omega
  have hB0 : 0 ≤ B := by
    have : 0 ≤ Real.log X := Real.log_nonneg (by exact_mod_cast hX1)
    positivity
  have hmain : (X : ℝ) * 2 ^ m ≤ b * B + X := by
    calc (X : ℝ) * 2 ^ m = ∑ t ∈ Finset.range X, (2 : ℝ) ^ m := by simp
      _ ≤ ∑ t ∈ Finset.range X, Tail f b (c + t * Q + m) := Finset.sum_le_sum fun t _ => hlow t
      _ ≤ ∑ t ∈ Finset.range X, (b * ∑ i ∈ Finset.range L, (f (c + m + i + 1 + t * Q) : ℝ) / 2 ^ (i + 1)
            + b * ((2 * X ^ 2 : ℕ) / 2 ^ L : ℝ)) :=
          Finset.sum_le_sum fun t ht => hupt t (by simpa using ht)
      _ = b * ∑ i ∈ Finset.range L, (∑ t ∈ Finset.range X, (f (c + m + i + 1 + t * Q) : ℝ)) * (1 / 2) ^ (i + 1)
            + X * (b * ((2 * X ^ 2 : ℕ) / 2 ^ L : ℝ)) := by
          rw [Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_comm]
          simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul, Finset.sum_mul, div_eq_mul_inv,
            inv_pow, one_mul]
      _ ≤ b * ∑ i ∈ Finset.range L, B * (1 / 2) ^ (i + 1) + X * 1 := by
          apply add_le_add
          · apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
            apply Finset.sum_le_sum
            intro i hi
            exact mul_le_mul_of_nonneg_right (hF i hi) (by positivity)
          · apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
            rw [← mul_div_assoc, div_le_one (by positivity)]
            have h1 : b * (2 * X ^ 2) ≤ 2 ^ L := by
              calc b * (2 * X ^ 2) = 2 * b * X ^ 2 := by ring
                _ ≤ 2 ^ L := hLX
            exact_mod_cast h1
      _ ≤ b * B + X := by
          rw [← Finset.mul_sum, mul_one]
          apply add_le_add_left
          apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
          calc B * ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1) ≤ B * 1 :=
                mul_le_mul_of_nonneg_left (hgeom L) hB0
            _ = B := mul_one B
  have hXpos : (0 : ℝ) < X := by exact_mod_cast hX1
  have h2m : (2 : ℝ) ^ m ≤ 2 * b * (2 + Real.log X) + 1 := by
    have : (X : ℝ) * 2 ^ m ≤ X * (2 * b * (2 + Real.log X) + 1) := by
      rw [hBdef] at hmain; nlinarith
    exact le_of_mul_le_mul_left this hXpos
  have hlogX : Real.log X ≤ q + 1 := by
    calc Real.log X ≤ Real.log ((2 : ℝ) ^ (q + 1)) :=
          Real.log_le_log hXpos (by exact_mod_cast hXpow)
      _ = (q + 1) * Real.log 2 := by rw [Real.log_pow]; push_cast; ring
      _ ≤ (q + 1) * 1 := by
          gcongr
          linarith [Real.log_two_lt_d9]
      _ = q + 1 := mul_one _
  have hA4' : (2 * b * (3 + q) + 1 : ℝ) < 2 ^ m := by exact_mod_cast hA4
  have : (2 * b * (2 + Real.log X) + 1 : ℝ) ≤ 2 * b * (3 + q) + 1 := by
    have : (0 : ℝ) ≤ b := by positivity
    nlinarith
  linarith

theorem variant_5274cf38__h1 : ∀ (B : Set ℕ),
  B.Nonempty →
    (∃ (p : ℕ), (0 : ℕ) < p ∧ ∀ (n : ℕ), n ∈ B ↔ n + p ∈ B) →
      Irrational (∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ))) := by
  -- approach: Erdős 1948 for A = ℕ with f_B(m) = #{d | m : d ∈ B} for d(m): Lambert identity, primes ≡ 1 mod the period placed by CRT force 2^m | f_B on windows along a progression, the divisor average bounds the tails; needs m² such primes in (2^m, 2^(m+m²)], a quantitative Dirichlet
  -- licence: CC-BY-4.0
  -- label: Lambert identity for a set
  -- claim: $\forall B \subseteq \mathbb{N}:\ \sum_{n \in B} \frac{1}{2^n - 1} = \sum_{m \ge 0} \frac{f_B(m)}{2^m},\ \text{where } f_B(m) = \#\{d \mid m : d \in B\} \text{ (both } 0 \text{ terms vanish)}$
  -- Expand 1/(2^n - 1) = Σ_{k ≥ 1} 2^{-nk} and collect the terms with nk = m; Mathlib has it for B = ℕ as `tsum_pow_div_one_sub_eq_tsum_sigma`.
  have hlam : ∀ B : Set ℕ, ∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ))
      = ∑' m : ℕ, (Set.ncard {d : ℕ | d ∈ m.divisors ∧ d ∈ B} : ℝ) / 2 ^ m := by
    intro B
    classical
    rw [lambert_set B]
    exact tsum_congr (fun m => by rw [fB_eq_ncard])
  -- label: primes ≡ 1 mod the period double f_B
  -- claim: $B \text{ purely periodic with period } P,\ n \ne 0,\ S \text{ a set of primes } p \equiv 1 \pmod P \text{ with } p \mid n,\ p^2 \nmid n\ \Rightarrow\ 2^{|S|} \mid f_B(n)$
  -- Write n = (∏_{p ∈ S} p) · r. A divisor of n is (∏_{p ∈ I} p) · d with I ⊆ S and d | r, and it is ≡ d (mod P), so it lies in B iff d does: f_B(n) = 2^{|S|} f_B(r).
  have hdvd : ∀ B : Set ℕ, ∀ P : ℕ, 0 < P → (∀ n, n ∈ B ↔ n + P ∈ B) →
      ∀ n : ℕ, n ≠ 0 → ∀ S : Finset ℕ,
      (∀ p ∈ S, p.Prime ∧ p % P = 1 ∧ p ∣ n ∧ ¬ p ^ 2 ∣ n) →
      2 ^ S.card ∣ Set.ncard {d : ℕ | d ∈ n.divisors ∧ d ∈ B} := by
    intro B P hP hper n hn S hS
    classical
    rw [← fB_eq_ncard]
    exact pow_two_dvd_fB B hP hper S n hn hS
  -- label: m² primes ≡ 1 mod P between 2^m and 2^(m+m²)
  -- claim: $\forall P \ge 1\ \exists m_0\ \forall m \ge m_0\ \exists S \subseteq \mathbb{P},\ |S| = m^2,\ \forall p \in S:\ p \equiv 1 \pmod P,\ 2^m < p \le 2^{m + m^2}$
  -- A weak quantitative Dirichlet theorem: the prime number theorem in arithmetic progressions gives ≍ 2^{m+m²}/(φ(P) m²) such primes. Mathlib has Dirichlet's theorem only qualitatively; the cyclotomic argument gives a prime ≡ 1 mod n below (n+1)^n, which is too sparse for the averaging step.
  have hprimes : ∀ P : ℕ, 0 < P → ∃ m₀ : ℕ, ∀ m : ℕ, m₀ ≤ m → ∃ S : Finset ℕ, S.card = m * m ∧
      ∀ p ∈ S, p.Prime ∧ p % P = 1 ∧ 2 ^ m < p ∧ p ≤ 2 ^ (m + m * m) := by
    sorry
  intro B hB ⟨P, hP, hper⟩
  classical
  obtain ⟨r, hr⟩ := hB
  have hfle : ∀ n, fB B n ≤ n := fB_le B
  have hfdd : ∀ n, fB B n ≤ dd n := fB_le_dd B
  have hposB : ∀ j, ∃ i, 0 < fB B (j + i + 1) := by
    intro j
    obtain ⟨i, hi⟩ := exists_mem_gt hP hper hr j
    exact ⟨i, fB_pos B (by omega) hi⟩
  have hx' : ∑' m : ℕ, (Set.ncard {d : ℕ | d ∈ m.divisors ∧ d ∈ B} : ℝ) / 2 ^ m
      = ∑' m : ℕ, (fB B m : ℝ) / 2 ^ m :=
    tsum_congr (fun m => by rw [fB_eq_ncard])
  rw [hlam B, hx']
  rintro ⟨qr, hq⟩
  set a : ℤ := qr.num
  set b : ℕ := qr.den
  have hb : 0 < b := qr.pos
  have hx : ∑' n : ℕ, (fB B n : ℝ) / 2 ^ n = a / b := by
    rw [← hq]; exact Rat.cast_def qr
  have hT : ∀ j, Tail (fB B) b j = Zint (fB B) a b j := tail_eq_Zint hfle hb hx
  obtain ⟨m₀, hm₀⟩ := hprimes P hP
  obtain ⟨m, hbm, hmm₀, hm1, hm⟩ := exists_param b m₀
  obtain ⟨hA1, hA2, hA3, hA4⟩ := param_facts hbm hm1 hm
  set q := 2 * (m + m * m) * (m * m) with hqdef
  obtain ⟨T, hTcard, hTp⟩ := hm₀ m hmm₀
  set S : Finset (ℕ × ℕ) := Finset.range m ×ˢ Finset.range m with hSdef
  have hmemS : ∀ ij ∈ S, ij.1 * m + ij.2 < m * m := by
    intro ij hij
    simp only [hSdef, Finset.mem_product, Finset.mem_range] at hij
    nlinarith
  -- the primes, indexed by position `i` and slot `j`
  obtain ⟨pr, hprp, hprT, hinj⟩ : ∃ pr : ℕ × ℕ → ℕ, (∀ ij, (pr ij).Prime) ∧
      (∀ ij ∈ S, pr ij ∈ T) ∧ Set.InjOn pr (S : Set (ℕ × ℕ)) := by
    refine ⟨fun ij => if h : ij.1 * m + ij.2 < m * m then T.orderEmbOfFin hTcard ⟨_, h⟩ else 2,
      ?_, ?_, ?_⟩
    · intro ij
      dsimp only
      split_ifs with h
      · exact (hTp _ (Finset.orderEmbOfFin_mem T hTcard _)).1
      · exact Nat.prime_two
    · intro ij hij
      dsimp only
      rw [dif_pos (hmemS ij hij)]
      exact Finset.orderEmbOfFin_mem T hTcard _
    · intro x hx y hy hxy
      have hx' := hmemS x hx
      have hy' := hmemS y hy
      dsimp only at hxy
      rw [dif_pos hx', dif_pos hy'] at hxy
      have h1 : x.1 * m + x.2 = y.1 * m + y.2 := by
        have := (T.orderEmbOfFin hTcard).injective hxy
        simpa using this
      simp only [hSdef, Finset.coe_product, Finset.coe_range, Set.mem_prod, Set.mem_Iio] at hx hy
      obtain ⟨e1, e2⟩ := idx_inj hx.2 hy.2 h1
      exact Prod.ext e1 e2
  have hprlo : ∀ ij ∈ S, 2 ^ m < pr ij := fun ij hij => (hTp _ (hprT ij hij)).2.2.1
  have hprhi : ∀ ij ∈ S, pr ij ≤ 2 ^ (m + m * m) := fun ij hij => (hTp _ (hprT ij hij)).2.2.2
  have hprmod : ∀ ij ∈ S, pr ij % P = 1 := fun ij hij => (hTp _ (hprT ij hij)).2.1
  set Q : ℕ := ∏ ij ∈ S, pr ij ^ 2 with hQdef
  have hQpos : 0 < Q := Finset.prod_pos (fun ij _ => pow_pos (hprp ij).pos 2)
  have hQle : Q ≤ 2 ^ q := by
    calc Q ≤ ((2 ^ (m + m * m)) ^ 2) ^ S.card := by
          apply Finset.prod_le_pow_card
          intro ij hij
          exact Nat.pow_le_pow_left (hprhi ij hij) 2
      _ = 2 ^ q := by
          rw [hSdef, Finset.card_product, Finset.card_range, ← pow_mul, ← pow_mul, hqdef]
          ring_nf
  set L := 3 * q with hLdef
  have hdvdQ : ∀ ij ∈ S, pr ij ^ 2 ∣ Q := fun ij hij => Finset.dvd_prod_of_mem _ hij
  -- Chinese remainder theorem
  have hs : ∀ ij ∈ S, pr ij ^ 2 ≠ 0 := fun ij _ => (pow_pos (hprp ij).pos 2).ne'
  have pp : Set.Pairwise (S : Set (ℕ × ℕ)) (Function.onFun Nat.Coprime fun ij => pr ij ^ 2) := by
    intro x hx y hy hxy
    exact Nat.Coprime.pow 2 2 ((Nat.coprime_primes (hprp x) (hprp y)).2
      (fun h => hxy (hinj hx hy h)))
  set crt := Nat.chineseRemainderOfFinset (fun ij => pr ij ^ 2 + pr ij - (ij.1 + 1))
    (fun ij => pr ij ^ 2) S hs pp
  set c : ℕ := crt.1
  have hc : ∀ ij ∈ S, c ≡ pr ij ^ 2 + pr ij - (ij.1 + 1) [MOD pr ij ^ 2] := crt.2
  have hcQ : c < Q := Nat.chineseRemainderOfFinset_lt_prod _ _ hs pp
  -- the key congruence
  have hk : ∀ t, ∀ ij ∈ S, c + t * Q + (ij.1 + 1) ≡ pr ij [MOD pr ij ^ 2] := by
    intro t ij hij
    obtain ⟨R, hR⟩ := hdvdQ ij hij
    have hi : ij.1 < m := by
      simp only [hSdef, Finset.mem_product, Finset.mem_range] at hij; exact hij.1
    have hp := hprlo ij hij
    have hm2 : m < 2 ^ m := Nat.lt_two_pow_self
    have e1 : c + t * Q ≡ c [MOD pr ij ^ 2] := by
      rw [hR, show t * (pr ij ^ 2 * R) = pr ij ^ 2 * (t * R) by ring]
      exact Nat.add_mul_mod_self_left _ _ _
    have e2 := (e1.trans (hc ij hij)).add_right (ij.1 + 1)
    rw [Nat.sub_add_cancel (by nlinarith)] at e2
    refine e2.trans ?_
    exact Nat.add_mod_left _ _
  -- forced divisibility
  have hforced : ∀ t, ∀ n, c + t * Q < n → n ≤ c + t * Q + m → 2 ^ m ∣ fB B n := by
    intro t n hn1 hn2
    obtain ⟨i, rfl⟩ : ∃ i, n = c + t * Q + (i + 1) := ⟨n - (c + t * Q) - 1, by omega⟩
    have hi : i < m := by omega
    have hcard : ((Finset.range m).image (fun j => pr (i, j))).card = m := by
      rw [Finset.card_image_of_injOn, Finset.card_range]
      intro j hj j' hj' h
      have := hinj (by simp [hSdef, hi, (by simpa using hj : j < m)])
        (by simp [hSdef, hi, (by simpa using hj' : j' < m)]) h
      simpa using this
    rw [fB_eq_ncard, ← hcard]
    apply hdvd B P hP hper _ (by omega)
    intro p hp
    obtain ⟨j, hj, rfl⟩ := Finset.mem_image.mp hp
    have hij : (i, j) ∈ S := by simp [hSdef, hi, (by simpa using hj : j < m)]
    have h := hk t (i, j) hij
    have hpp := hprp (i, j)
    refine ⟨hpp, hprmod _ hij, (h.dvd_iff (Dvd.intro_left _ (pow_two _).symm)).2 dvd_rfl, ?_⟩
    rw [h.dvd_iff dvd_rfl]
    intro hd
    have := Nat.le_of_dvd hpp.pos hd
    have := hpp.two_le
    nlinarith
  -- coprimality
  have hcop : ∀ i < L, Nat.Coprime (c + m + i + 1) Q := by
    intro i hi
    apply Nat.Coprime.prod_right
    intro ij hij
    apply Nat.Coprime.pow_right
    rw [Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd (hprp ij)]
    intro hd
    have hi0 : ij.1 < m := by
      simp only [hSdef, Finset.mem_product, Finset.mem_range] at hij; exact hij.1
    have h1 : pr ij ∣ c + 0 * Q + (ij.1 + 1) :=
      ((hk 0 ij hij).dvd_iff (Dvd.intro_left _ (pow_two _).symm)).2 dvd_rfl
    have h2 : c + m + i + 1 = (c + 0 * Q + (ij.1 + 1)) + (m + i - ij.1) := by omega
    rw [h2] at hd
    have h3 := (Nat.dvd_add_right h1).mp hd
    have h4 := Nat.le_of_dvd (by omega) h3
    have := hprlo ij hij
    omega
  -- lower bound
  have hlow : ∀ t, (2 : ℝ) ^ m ≤ Tail (fB B) b (c + t * Q + m) := by
    intro t
    have hd := Zint_dvd (fB B) a b (c + t * Q) m (hforced t)
    obtain ⟨i₀, hi₀⟩ := hposB (c + t * Q + m)
    have hpos := tail_pos hfle hb (c + t * Q + m) hi₀
    rw [hT] at hpos ⊢
    have hpos' : 0 < Zint (fB B) a b (c + t * Q + m) := by exact_mod_cast hpos
    have := Int.le_of_dvd hpos' hd
    exact_mod_cast this
  exact averaging_contra hfdd hb hQpos hcQ hQle hA2 hA3 hA4 hcop hlow

Untrusted contributor text — a partial assembly: it records an attempt, and no attestation covers it.

Untrusted: partial assembly (D-12 #5), author not recorded; no postmortem record names this file. No attestation covers a partial — it records an attempt, not a proof. Rendered from targets/erdos-257/nodes/variant-5274cf38--h1/attempts/20261026T214903Z-t1026-b-partial.lean.

import Mathlib
import Nodes.«variant-5274cf38--h1».Context

/-! Hole `hper` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

/- The divisor-counting function. -/
private def dd (n : ℕ) : ℕ := n.divisors.card

/- `f_B(n)`: the number of divisors of `n` that lie in `B`. -/
private def fB (B : Set ℕ) [DecidablePred (· ∈ B)] (n : ℕ) : ℕ :=
  (n.divisors.filter (· ∈ B)).card

private lemma fB_eq_ncard (B : Set ℕ) [DecidablePred (· ∈ B)] (n : ℕ) :
    fB B n = Set.ncard {d : ℕ | d ∈ n.divisors ∧ d ∈ B} := by
  unfold fB
  rw [← Set.ncard_coe_finset]
  congr 1
  ext d
  simp

private lemma fB_le_dd (B : Set ℕ) [DecidablePred (· ∈ B)] (n : ℕ) : fB B n ≤ dd n :=
  Finset.card_filter_le _ _

private lemma fB_le (B : Set ℕ) [DecidablePred (· ∈ B)] (n : ℕ) : fB B n ≤ n :=
  (fB_le_dd B n).trans (Nat.card_divisors_le_self n)

private lemma fB_pos (B : Set ℕ) [DecidablePred (· ∈ B)] {n : ℕ} (hn : n ≠ 0) (hnB : n ∈ B) :
    0 < fB B n := by
  unfold fB
  exact Finset.card_pos.mpr ⟨n, by simp [Finset.mem_filter, Nat.mem_divisors, hn, hnB]⟩

/- A periodic set has an element beyond every `j`. -/
private lemma exists_mem_gt {B : Set ℕ} {P : ℕ} (hP : 0 < P)
    (hper : ∀ n, n ∈ B ↔ n + P ∈ B) {r : ℕ} (hr : r ∈ B) (j : ℕ) : ∃ i, j + i + 1 ∈ B := by
  have hiter : ∀ k, r + P * k ∈ B := by
    intro k
    induction k with
    | zero => simpa using hr
    | succ k ih =>
      rw [show r + P * (k + 1) = (r + P * k) + P by ring]
      exact (hper _).1 ih
  refine ⟨r + P * (j + 1) - j - 1, ?_⟩
  have : j + 1 ≤ r + P * (j + 1) := by nlinarith
  rw [show j + (r + P * (j + 1) - j - 1) + 1 = r + P * (j + 1) by omega]
  exact hiter _

/- `b` times the "tail" `∑_{i ≥ 1} f(j+i) / 2^i`. -/
private noncomputable def Tail (f : ℕ → ℕ) (b : ℕ) (j : ℕ) : ℝ :=
  b * ∑' i : ℕ, (f (j + i + 1) : ℝ) / 2 ^ (i + 1)

/- The integer that the tail equals when the series is `a / b`. -/
private def Zint (f : ℕ → ℕ) (a : ℤ) (b : ℕ) (j : ℕ) : ℤ :=
  a * 2 ^ j - b * ∑ n ∈ Finset.range (j + 1), (f n : ℤ) * 2 ^ (j - n)

private lemma summable_shift {f : ℕ → ℕ} (hf : ∀ n, f n ≤ n) (j : ℕ) :
    Summable (fun i : ℕ => (f (j + i + 1) : ℝ) / 2 ^ (i + 1)) := by
  have h : Summable (fun i : ℕ => ((j + 1 : ℝ) + i) * (1/2) ^ i) := by
    have h1 := (summable_geometric_two).mul_left (j+1 : ℝ)
    have h2 := summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
      (by norm_num [abs_of_pos])
    simpa [add_mul] using h1.add h2
  refine Summable.of_nonneg_of_le (fun i => by positivity) (fun i => ?_) h
  have : (f (j + i + 1) : ℝ) ≤ j + i + 1 := by exact_mod_cast hf _
  rw [div_eq_mul_inv, pow_succ, mul_inv, one_div, inv_pow]
  have : (0:ℝ) ≤ (2 ^ i)⁻¹ := by positivity
  nlinarith

private lemma summable_f {f : ℕ → ℕ} (hf : ∀ n, f n ≤ n) :
    Summable (fun n : ℕ => (f n : ℝ) / 2 ^ n) := by
  have h2 := summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
    (by norm_num [abs_of_pos])
  refine Summable.of_nonneg_of_le (fun i => by positivity) (fun i => ?_) h2
  have : (f i : ℝ) ≤ i := by exact_mod_cast hf _
  rw [div_eq_mul_inv, one_div, inv_pow, pow_one]
  have : (0:ℝ) ≤ (2 ^ i)⁻¹ := by positivity
  nlinarith

private lemma tail_pos {f : ℕ → ℕ} (hf : ∀ n, f n ≤ n) {b : ℕ} (hb : 0 < b) (j : ℕ)
    {i₀ : ℕ} (hi₀ : 0 < f (j + i₀ + 1)) : 0 < Tail f b j := by
  unfold Tail
  apply mul_pos (by exact_mod_cast hb)
  apply (summable_shift hf j).tsum_pos (fun i => by positivity) i₀
  positivity

private lemma tail_upper {f : ℕ → ℕ} (hf : ∀ n, f n ≤ n) (b j L : ℕ) :
    Tail f b j ≤ b * ∑ i ∈ Finset.range L, (f (j + i + 1) : ℝ) / 2 ^ (i + 1)
      + b * ((j + L + 2 : ℝ) / 2 ^ L) := by
  unfold Tail
  rw [← (summable_shift hf j).sum_add_tsum_nat_add L, mul_add]
  gcongr
  have hg1 : Summable (fun i : ℕ => (1/2 : ℝ) ^ i) := summable_geometric_two
  have hg2 : Summable (fun i : ℕ => (i : ℝ) * (1/2 : ℝ) ^ i) := by
    simpa using summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
      (by norm_num [abs_of_pos])
  have key : ∑' i : ℕ, ((j + L + 1 : ℝ) / 2 ^ (L + 1) * (1/2) ^ i
      + 1 / 2 ^ (L + 1) * ((i : ℝ) * (1/2) ^ i)) = (j + L + 2 : ℝ) / 2 ^ L := by
    rw [(hg1.mul_left _).tsum_add (hg2.mul_left _), tsum_mul_left, tsum_mul_left,
      tsum_geometric_two, tsum_coe_mul_geometric_of_norm_lt_one (by norm_num [abs_of_pos])]
    rw [pow_succ]; field_simp; ring
  rw [← key]
  refine Summable.tsum_le_tsum (fun i => ?_) ((summable_nat_add_iff L).mpr (summable_shift hf j))
    ((hg1.mul_left _).add (hg2.mul_left _))
  have : (f (j + (i + L) + 1) : ℝ) ≤ j + L + 1 + i := by
    have := hf (j + (i + L) + 1)
    have : (f (j + (i + L) + 1) : ℝ) ≤ ((j + (i + L) + 1 : ℕ) : ℝ) := by exact_mod_cast this
    push_cast at this; linarith
  show (f (j + (i + L) + 1) : ℝ) / 2 ^ (i + L + 1) ≤ _
  rw [show (2:ℝ) ^ (i + L + 1) = 2 ^ (L+1) * 2 ^ i by ring, one_div_pow]
  rw [div_le_iff₀ (by positivity)]
  field_simp
  linarith

private lemma tail_eq_Zint {f : ℕ → ℕ} (hf : ∀ n, f n ≤ n) {a : ℤ} {b : ℕ} (hb : 0 < b)
    (h : ∑' n : ℕ, (f n : ℝ) / 2 ^ n = a / b) (j : ℕ) : Tail f b j = Zint f a b j := by
  have hsplit := (summable_f hf).sum_add_tsum_nat_add (j + 1)
  have htail : ∑' i : ℕ, (f (i + (j + 1)) : ℝ) / 2 ^ (i + (j + 1)) =
      (1 / 2 ^ j) * ∑' i : ℕ, (f (j + i + 1) : ℝ) / 2 ^ (i + 1) := by
    rw [← tsum_mul_left]
    apply tsum_congr; intro i
    rw [show i + (j + 1) = j + i + 1 by ring,
      show (2:ℝ) ^ (j + i + 1) = 2 ^ j * 2 ^ (i + 1) by ring]
    field_simp
  rw [htail, h] at hsplit
  have hb' : (b : ℝ) ≠ 0 := by exact_mod_cast hb.ne'
  have hT : Tail f b j = 2 ^ j * (a - b * ∑ n ∈ Finset.range (j + 1), (f n : ℝ) / 2 ^ n) := by
    unfold Tail
    field_simp at hsplit
    have : (2:ℝ) ^ j ≠ 0 := by positivity
    field_simp
    linear_combination hsplit
  rw [hT]
  unfold Zint
  push_cast
  rw [mul_sub, Finset.mul_sum, Finset.mul_sum, Finset.mul_sum]
  congr 1
  · ring
  · apply Finset.sum_congr rfl; intro n hn
    have hn' : n ≤ j := Nat.lt_succ_iff.mp (Finset.mem_range.mp hn)
    rw [pow_sub₀ _ (by norm_num) hn']
    field_simp

private lemma Zint_dvd (f : ℕ → ℕ) (a : ℤ) (b k m : ℕ)
    (hd : ∀ n, k < n → n ≤ k + m → 2 ^ m ∣ f n) :
    (2 : ℤ) ^ m ∣ Zint f a b (k + m) := by
  unfold Zint
  apply dvd_sub
  · exact Dvd.dvd.mul_left (pow_dvd_pow 2 (by omega)) _
  · apply Dvd.dvd.mul_left
    apply Finset.dvd_sum
    intro n hn
    have hn' : n ≤ k + m := Nat.lt_succ_iff.mp (Finset.mem_range.mp hn)
    by_cases hnk : n ≤ k
    · exact Dvd.dvd.mul_left (pow_dvd_pow 2 (by omega)) _
    · apply Dvd.dvd.mul_right
      exact_mod_cast hd n (by omega) hn'

private lemma dd_le_two_mul_small (n : ℕ) :
    dd n ≤ 2 * (n.divisors.filter (fun e => e * e ≤ n)).card := by
  unfold dd
  rw [← Finset.card_filter_add_card_filter_not (fun e => e * e ≤ n)]
  have : (n.divisors.filter (fun e => ¬ e * e ≤ n)).card ≤
      (n.divisors.filter (fun e => e * e ≤ n)).card := by
    apply Finset.card_le_card_of_injOn (fun e => n / e)
    · intro e he
      simp only [Finset.coe_filter, Nat.mem_divisors, not_le, Set.mem_setOf_eq] at he ⊢
      obtain ⟨⟨hd, hn⟩, hlt⟩ := he
      have hepos : 0 < e := Nat.pos_of_dvd_of_pos hd (Nat.pos_of_ne_zero hn)
      refine ⟨⟨Nat.div_dvd_of_dvd hd, hn⟩, ?_⟩
      have h1 : n / e < e := (Nat.div_lt_iff_lt_mul hepos).mpr hlt
      calc n / e * (n / e) ≤ n / e * e := Nat.mul_le_mul_left _ h1.le
        _ = n := Nat.div_mul_cancel hd
    · intro e1 h1 e2 h2 h
      simp only [Finset.coe_filter, Nat.mem_divisors, Set.mem_setOf_eq] at h1 h2
      have := congrArg (fun x => n / x) h
      simp only at this
      rwa [Nat.div_div_self h1.1.1 h1.1.2, Nat.div_div_self h2.1.1 h2.1.2] at this
  omega

private lemma card_AP_dvd_le (r Q X e : ℕ) (hcop : Nat.Coprime r Q) :
    ((Finset.range X).filter (fun t => (e + 1) ∣ r + t * Q)).card ≤ X / (e + 1) + 1 := by
  set E := e + 1 with hE
  have hEpos : 0 < E := by omega
  have key : ∀ t1 ∈ (Finset.range X).filter (fun t => E ∣ r + t * Q),
      ∀ t2 ∈ (Finset.range X).filter (fun t => E ∣ r + t * Q), t1 / E = t2 / E → t1 ≤ t2 → t1 = t2 := by
    intro t1 h1 t2 h2 hq hle
    simp only [Finset.mem_filter, Finset.mem_range] at h1 h2
    have hcopE : Nat.Coprime E Q := by
      have hg1 : Nat.gcd E Q ∣ r + t1 * Q := (Nat.gcd_dvd_left E Q).trans h1.2
      have hg2 : Nat.gcd E Q ∣ t1 * Q := Dvd.dvd.mul_left (Nat.gcd_dvd_right E Q) _
      have hg3 : Nat.gcd E Q ∣ r := (Nat.dvd_add_left hg2).mp hg1
      have hg4 : Nat.gcd E Q ∣ Nat.gcd r Q := Nat.dvd_gcd hg3 (Nat.gcd_dvd_right E Q)
      rw [hcop] at hg4
      exact Nat.dvd_one.mp hg4
    have hd : E ∣ (t2 - t1) * Q := by
      have := Nat.dvd_sub h2.2 h1.2
      rwa [show r + t2 * Q - (r + t1 * Q) = (t2 - t1) * Q by rw [Nat.sub_mul]; omega] at this
    have hd2 : E ∣ t2 - t1 := hcopE.dvd_of_dvd_mul_right hd
    have hlt : t2 - t1 < E := by
      have e1 := Nat.div_add_mod t1 E
      have e2 := Nat.div_add_mod t2 E
      have m1 := Nat.mod_lt t1 hEpos
      have m2 := Nat.mod_lt t2 hEpos
      rw [hq] at e1
      omega
    have := Nat.eq_zero_of_dvd_of_lt hd2 hlt
    omega
  calc ((Finset.range X).filter (fun t => E ∣ r + t * Q)).card ≤ (Finset.range (X / E + 1)).card := by
        apply Finset.card_le_card_of_injOn (fun t => t / E)
        · intro t ht
          simp only [Finset.coe_filter, Finset.mem_range, Set.mem_setOf_eq] at ht
          simp only [Finset.coe_range, Set.mem_Iio]
          have := Nat.div_le_div_right (c := E) ht.1.le
          omega
        · intro t1 h1 t2 h2 hq
          rcases le_total t1 t2 with h | h
          · exact key t1 h1 t2 h2 hq h
          · exact (key t2 h2 t1 h1 hq.symm h).symm
    _ = X / E + 1 := Finset.card_range _

private lemma sum_dd_AP_le (r Q X : ℕ) (hcop : Nat.Coprime r Q)
    (hX : ∀ t < X, r + t * Q ≤ X * X) :
    (∑ t ∈ Finset.range X, (dd (r + t * Q) : ℝ)) ≤ 2 * X * (2 + Real.log X) := by
  have hnat : ∑ t ∈ Finset.range X, dd (r + t * Q) ≤ 2 * ∑ e ∈ Finset.range X, (X / (e + 1) + 1) := by
    calc ∑ t ∈ Finset.range X, dd (r + t * Q)
        ≤ ∑ t ∈ Finset.range X, 2 * ((Finset.range X).filter (fun e => (e + 1) ∣ r + t * Q)).card := by
          apply Finset.sum_le_sum; intro t ht
          refine (dd_le_two_mul_small _).trans ?_
          apply Nat.mul_le_mul_left
          apply Finset.card_le_card_of_injOn (fun e => e - 1)
          · intro e he
            simp only [Finset.coe_filter, Nat.mem_divisors, Set.mem_setOf_eq] at he
            simp only [Finset.coe_filter, Finset.mem_range, Set.mem_setOf_eq]
            have hepos : 0 < e := Nat.pos_of_dvd_of_pos he.1.1 (Nat.pos_of_ne_zero he.1.2)
            have : e * e ≤ X * X := he.2.trans (hX t (by simpa using ht))
            have : e ≤ X := Nat.mul_self_le_mul_self_iff.mp this
            refine ⟨by omega, ?_⟩
            rw [Nat.sub_add_cancel hepos]; exact he.1.1
          · intro e1 h1 e2 h2 h
            simp only [Finset.coe_filter, Nat.mem_divisors, Set.mem_setOf_eq] at h1 h2
            have := Nat.pos_of_dvd_of_pos h1.1.1 (Nat.pos_of_ne_zero h1.1.2)
            have := Nat.pos_of_dvd_of_pos h2.1.1 (Nat.pos_of_ne_zero h2.1.2)
            simp only at h
            omega
      _ = 2 * ∑ e ∈ Finset.range X, ((Finset.range X).filter (fun t => (e + 1) ∣ r + t * Q)).card := by
          rw [← Finset.mul_sum]
          congr 1
          simp only [Finset.card_filter]
          exact Finset.sum_comm
      _ ≤ 2 * ∑ e ∈ Finset.range X, (X / (e + 1) + 1) := by
          apply Nat.mul_le_mul_left
          exact Finset.sum_le_sum fun e _ => card_AP_dvd_le r Q X e hcop
  have hreal : ((∑ e ∈ Finset.range X, (X / (e + 1) + 1) : ℕ) : ℝ) ≤ X * (1 + Real.log X) + X := by
    push_cast
    rw [Finset.sum_add_distrib]
    simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_one]
    gcongr
    calc ∑ e ∈ Finset.range X, ((X / (e + 1) : ℕ) : ℝ) ≤ ∑ e ∈ Finset.range X, (X : ℝ) / (e + 1) := by
          apply Finset.sum_le_sum; intro e _
          have := Nat.cast_div_le (α := ℝ) (m := X) (n := e + 1)
          push_cast at this; exact this
      _ = X * (harmonic X : ℝ) := by
          rw [harmonic]; push_cast; rw [Finset.mul_sum]
          apply Finset.sum_congr rfl; intro e _; field_simp
      _ ≤ X * (1 + Real.log X) := by
          gcongr
          exact harmonic_le_one_add_log X
  have h1 : (∑ t ∈ Finset.range X, (dd (r + t * Q) : ℝ)) ≤
      2 * ((∑ e ∈ Finset.range X, (X / (e + 1) + 1) : ℕ) : ℝ) := by
    exact_mod_cast hnat
  linarith

private lemma idx_inj {m i j i' j' : ℕ} (hj : j < m) (hj' : j' < m) (h : i * m + j = i' * m + j') :
    i = i' ∧ j = j' := by
  rcases lt_trichotomy i i' with hi | hi | hi
  · exfalso
    have : (i + 1) * m ≤ i' * m := Nat.mul_le_mul_right _ hi
    nlinarith
  · subst hi; omega
  · exfalso
    have : (i' + 1) * m ≤ i * m := Nat.mul_le_mul_right _ hi
    nlinarith


private lemma mem_iff_add_mul {B : Set ℕ} {P : ℕ} (hper : ∀ n, n ∈ B ↔ n + P ∈ B) (n k : ℕ) :
    n ∈ B ↔ n + P * k ∈ B := by
  induction k with
  | zero => simp
  | succ k ih =>
    rw [ih, hper (n + P * k), show n + P * k + P = n + P * (k + 1) by ring]

/- A prime `p ≡ 1 (mod P)` not dividing `r` doubles `f_B`: the divisors of `p r` are the
divisors `d` of `r` and the numbers `p d`, and `p d ≡ d (mod P)`. -/
private lemma fB_mul_prime (B : Set ℕ) [DecidablePred (· ∈ B)] {P : ℕ} (hP : 0 < P)
    (hper : ∀ n, n ∈ B ↔ n + P ∈ B) {p r : ℕ} (hp : p.Prime) (hpP : p % P = 1)
    (hpr : ¬ p ∣ r) (hr : r ≠ 0) : fB B (p * r) = 2 * fB B r := by
  have hpd : ∀ d, p * d = d + P * (p / P * d) := by
    intro d
    have := Nat.div_add_mod p P
    rw [hpP] at this
    calc p * d = (P * (p / P) + 1) * d := by rw [this]
      _ = d + P * (p / P * d) := by ring
  have hpB : ∀ d, p * d ∈ B ↔ d ∈ B := by
    intro d
    rw [hpd d]
    exact (mem_iff_add_mul hper d _).symm
  have hpr0 : p * r ≠ 0 := mul_ne_zero hp.ne_zero hr
  have hsplit : (p * r).divisors.filter (· ∈ B) =
      (r.divisors.filter (· ∈ B)) ∪
        ((r.divisors.filter (· ∈ B)).map ⟨(p * ·), mul_right_injective₀ hp.ne_zero⟩) := by
    ext D
    simp only [Finset.mem_filter, Nat.mem_divisors, Finset.mem_union, Finset.mem_map,
      Function.Embedding.coeFn_mk]
    constructor
    · rintro ⟨⟨hD, -⟩, hDB⟩
      by_cases hpD : p ∣ D
      · obtain ⟨d, rfl⟩ := hpD
        right
        refine ⟨d, ⟨⟨?_, hr⟩, (hpB d).1 hDB⟩, rfl⟩
        exact (Nat.mul_dvd_mul_iff_left hp.pos).1 hD
      · left
        refine ⟨⟨?_, hr⟩, hDB⟩
        exact Nat.Coprime.dvd_of_dvd_mul_left ((Nat.Prime.coprime_iff_not_dvd hp).2 hpD).symm hD
    · rintro (⟨⟨hD, -⟩, hDB⟩ | ⟨d, ⟨⟨hd, -⟩, hdB⟩, rfl⟩)
      · exact ⟨⟨dvd_mul_of_dvd_right hD p, hpr0⟩, hDB⟩
      · exact ⟨⟨mul_dvd_mul_left p hd, hpr0⟩, (hpB d).2 hdB⟩
  have hdisj : Disjoint (r.divisors.filter (· ∈ B))
      ((r.divisors.filter (· ∈ B)).map ⟨(p * ·), mul_right_injective₀ hp.ne_zero⟩) := by
    rw [Finset.disjoint_left]
    intro D hD hD'
    simp only [Finset.mem_filter, Nat.mem_divisors, Finset.mem_map,
      Function.Embedding.coeFn_mk] at hD hD'
    obtain ⟨d, -, rfl⟩ := hD'
    exact hpr (dvd_trans (dvd_mul_right p d) hD.1.1)
  unfold fB
  rw [hsplit, Finset.card_union_of_disjoint hdisj, Finset.card_map]
  ring

/- Each of `S`'s primes, `≡ 1 (mod P)` and dividing `n` exactly once, doubles `f_B`. -/
private lemma pow_two_dvd_fB (B : Set ℕ) [DecidablePred (· ∈ B)] {P : ℕ} (hP : 0 < P)
    (hper : ∀ n, n ∈ B ↔ n + P ∈ B) (S : Finset ℕ) : ∀ n : ℕ, n ≠ 0 →
    (∀ p ∈ S, p.Prime ∧ p % P = 1 ∧ p ∣ n ∧ ¬ p ^ 2 ∣ n) → 2 ^ S.card ∣ fB B n := by
  refine Finset.induction_on S ?_ ?_
  · intro n _ _
    simp
  · intro p S hpS ih n hn hS
    obtain ⟨hp, hpP, hpn, hp2⟩ := hS p (Finset.mem_insert_self _ _)
    obtain ⟨r, rfl⟩ := hpn
    have hr : r ≠ 0 := by
      rintro rfl
      simp at hn
    have hpr : ¬ p ∣ r := fun h => hp2 (by rw [pow_two]; exact mul_dvd_mul_left p h)
    rw [Finset.card_insert_of_notMem hpS, pow_succ, fB_mul_prime B hP hper hp hpP hpr hr,
      mul_comm (2 ^ S.card) 2]
    apply mul_dvd_mul_left 2
    apply ih r hr
    intro q hq
    obtain ⟨hqpr, hqP, hqn, hq2⟩ := hS q (Finset.mem_insert_of_mem hq)
    have hqp : q ≠ p := fun h => hpS (h ▸ hq)
    refine ⟨hqpr, hqP, ?_, ?_⟩
    · exact Nat.Coprime.dvd_of_dvd_mul_left ((Nat.coprime_primes hqpr hp).2 hqp) hqn
    · intro h
      exact hq2 (dvd_mul_of_dvd_right h p)

private lemma tsum_pnat_of_zero (f : ℕ → ℝ) (h0 : f 0 = 0) : ∑' n : ℕ+, f n = ∑' n : ℕ, f n := by
  apply Function.Injective.tsum_eq PNat.coe_injective
  intro n hn
  have : n ≠ 0 := by rintro rfl; exact hn h0
  exact ⟨⟨n, Nat.pos_of_ne_zero this⟩, rfl⟩

private lemma geom_pnat {x : ℝ} (hx : |x| < 1) : ∑' c : ℕ+, x ^ (c : ℕ) = x / (1 - x) := by
  rw [tsum_pnat_eq_tsum_succ (f := fun m : ℕ => x ^ m)]
  simp_rw [pow_succ]
  rw [tsum_mul_right, tsum_geometric_of_abs_lt_one hx]
  ring

/- The Lambert identity for a set: `∑_{n ∈ B} 1/(2^n - 1) = ∑_m f_B(m) / 2^m`. -/
private lemma lambert_set (B : Set ℕ) [DecidablePred (· ∈ B)] :
    ∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ))
      = ∑' m : ℕ, (fB B m : ℝ) / 2 ^ m := by
  set w : ℕ → ℝ := fun d => if d ∈ B then 1 else 0 with hw
  have hw01 : ∀ d, 0 ≤ w d ∧ w d ≤ 1 := fun d => by
    simp only [hw]; split_ifs <;> norm_num
  set r : ℝ := 1 / 2 with hr
  have hr1 : ‖r‖ < 1 := by rw [hr, Real.norm_eq_abs, abs_of_pos (by norm_num)]; norm_num
  set G : ℕ+ × ℕ+ → ℝ := fun c => w c.1 * r ^ ((c.1 : ℕ) * (c.2 : ℕ)) with hG
  have hGs : Summable G := by
    have h := summable_prod_mul_pow (𝕜 := ℝ) 0 hr1
    refine Summable.of_nonneg_of_le (fun c => ?_) (fun c => ?_) h
    · exact mul_nonneg (hw01 _).1 (by positivity)
    · simp only [pow_zero, one_mul]
      exact mul_le_of_le_one_left (by positivity) (hw01 _).2
  have hprod : ∑' c : ℕ+ × ℕ+, G c = ∑' d : ℕ+, w d / (2 ^ (d : ℕ) - 1) := by
    rw [hGs.tsum_prod]
    refine tsum_congr fun d => ?_
    simp only [hG]
    simp_rw [pow_mul]
    rw [tsum_mul_left, geom_pnat ?_]
    · have h3 : (2:ℝ) ^ (d:ℕ) - 1 ≠ 0 := by
        have : (1:ℝ) < 2 ^ (d:ℕ) := one_lt_pow₀ (by norm_num) d.ne_zero
        linarith
      rw [hr, one_div_pow]
      field_simp
    · rw [hr, one_div_pow, abs_of_pos (by positivity), div_lt_one (by positivity)]
      exact one_lt_pow₀ (by norm_num) d.ne_zero
  have hsig : ∑' c : ℕ+ × ℕ+, G c = ∑' e : ℕ+, (fB B e : ℝ) * r ^ (e : ℕ) := by
    rw [← sigmaAntidiagonalEquivProd.tsum_eq]
    have hs : Summable (fun x => G (sigmaAntidiagonalEquivProd x)) :=
      (Equiv.summable_iff _).2 hGs
    rw [hs.tsum_sigma]
    refine tsum_congr fun e => ?_
    rw [tsum_fintype]
    simp only [sigmaAntidiagonalEquivProd, divisorsAntidiagonalFactors, Equiv.coe_fn_mk,
      PNat.mk_coe, hG]
    rw [Finset.univ_eq_attach,
      (e : ℕ).divisorsAntidiagonal.sum_attach (fun x : ℕ × ℕ => w x.1 * r ^ (x.1 * x.2)),
      Nat.sum_divisorsAntidiagonal (fun a b => w a * r ^ (a * b))]
    rw [Finset.sum_congr rfl (fun a ha => by
      rw [Nat.mul_div_cancel' (Nat.dvd_of_mem_divisors ha)] :
        ∀ a ∈ (e : ℕ).divisors, w a * r ^ (a * ((e : ℕ) / a)) = w a * r ^ (e : ℕ))]
    rw [← Finset.sum_mul]
    congr 1
    unfold fB
    rw [Finset.card_filter]
    push_cast
    rfl
  have hL : ∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ))
      = ∑' d : ℕ+, w d / (2 ^ (d : ℕ) - 1) := by
    rw [tsum_subtype B (fun n : ℕ => (1 : ℝ) / ((2:ℝ) ^ n - 1))]
    rw [tsum_pnat_of_zero (fun n : ℕ => w n / (2 ^ n - 1)) (by simp)]
    refine tsum_congr fun n => ?_
    simp only [Set.indicator_apply, hw]
    split_ifs <;> simp
  have hR : ∑' m : ℕ, (fB B m : ℝ) / 2 ^ m = ∑' e : ℕ+, (fB B e : ℝ) * r ^ (e : ℕ) := by
    rw [← tsum_pnat_of_zero (fun m : ℕ => (fB B m : ℝ) / 2 ^ m) (by simp [fB])]
    refine tsum_congr fun e => ?_
    rw [hr, one_div_pow, div_eq_mul_inv, one_div]
  rw [hL, hR, ← hprod, ← hsig]

/- Submultiplicativity of the divisor count. -/
private lemma dd_mul_le (a b : ℕ) : dd (a * b) ≤ dd a * dd b := by
  unfold dd
  rw [Nat.divisors_mul]
  exact Finset.card_mul_le

private lemma dd_le_of_dvd {a b : ℕ} (hb : b ≠ 0) (h : a ∣ b) : dd a ≤ dd b :=
  Finset.card_le_card (Nat.divisors_subset_of_dvd hb h)

/- The divisor sum along a progression with any start, in terms of the gcd. -/
private lemma sum_dd_AP_le' (r Q X : ℕ) (hQ : 0 < Q)
    (hX : ∀ t < X, r + t * Q ≤ X * X) :
    (∑ t ∈ Finset.range X, (dd (r + t * Q) : ℝ)) ≤ dd (Nat.gcd r Q) * (2 * X * (2 + Real.log X)) := by
  set g := Nat.gcd r Q with hg
  have hgpos : 0 < g := Nat.gcd_pos_of_pos_right _ hQ
  obtain ⟨r', hr'⟩ : g ∣ r := Nat.gcd_dvd_left r Q
  obtain ⟨Q', hQ'⟩ : g ∣ Q := Nat.gcd_dvd_right r Q
  have hcop : Nat.Coprime r' Q' := by
    have h := Nat.coprime_div_gcd_div_gcd (m := r) (n := Q) hgpos
    have e1 : r / g = r' := by
      rw [hr']
      exact Nat.mul_div_cancel_left r' hgpos
    have e2 : Q / g = Q' := by
      rw [hQ']
      exact Nat.mul_div_cancel_left Q' hgpos
    rwa [e1, e2] at h
  have hsplit : ∀ t, r + t * Q = g * (r' + t * Q') := by
    intro t
    rw [hr', hQ']
    ring
  calc (∑ t ∈ Finset.range X, (dd (r + t * Q) : ℝ))
      ≤ ∑ t ∈ Finset.range X, (dd g : ℝ) * dd (r' + t * Q') := by
        apply Finset.sum_le_sum; intro t _
        rw [hsplit]; exact_mod_cast dd_mul_le _ (r' + t * Q')
    _ = dd g * ∑ t ∈ Finset.range X, (dd (r' + t * Q') : ℝ) := by rw [Finset.mul_sum]
    _ ≤ dd g * (2 * X * (2 + Real.log X)) := by
        gcongr
        apply sum_dd_AP_le r' Q' X hcop
        intro t ht
        have h := hX t ht
        rw [hsplit] at h
        calc r' + t * Q' ≤ g * (r' + t * Q') := Nat.le_mul_of_pos_left _ hgpos
          _ ≤ X * X := h

/- A geometric tail starting at `s` is at most `1`. -/
private lemma geom_tail_le (s L : ℕ) :
    ∑ i ∈ Finset.range L, (if s ≤ i then (1 / 2 : ℝ) ^ (i + 1 - s) else 0) ≤ 1 := by
  have hgeom : ∀ L : ℕ, ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1) ≤ 1 := by
    intro L
    have : ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1) = 1 - (1 / 2) ^ L := by
      induction L with
      | zero => simp
      | succ n ih => rw [Finset.sum_range_succ, ih]; ring
    rw [this]; linarith [pow_pos (by norm_num : (0 : ℝ) < 1 / 2) L]
  calc ∑ i ∈ Finset.range L, (if s ≤ i then (1 / 2 : ℝ) ^ (i + 1 - s) else 0)
      ≤ ∑ i ∈ Finset.range (s + L), (if s ≤ i then (1 / 2 : ℝ) ^ (i + 1 - s) else 0) := by
        apply Finset.sum_le_sum_of_subset_of_nonneg
        · exact Finset.range_mono (Nat.le_add_left L s)
        · intro i _ _; split_ifs <;> positivity
    _ = ∑ i ∈ Finset.range s, (if s ≤ i then (1 / 2 : ℝ) ^ (i + 1 - s) else 0)
          + ∑ j ∈ Finset.range L, (if s ≤ s + j then (1 / 2 : ℝ) ^ (s + j + 1 - s) else 0) :=
        Finset.sum_range_add _ s L
    _ = 0 + ∑ j ∈ Finset.range L, (1 / 2 : ℝ) ^ (j + 1) := by
        congr 1
        · apply Finset.sum_eq_zero
          intro i hi
          rw [if_neg (by simp at hi; omega)]
        · apply Finset.sum_congr rfl
          intro j _
          rw [if_pos (by omega), show s + j + 1 - s = j + 1 by omega]
    _ ≤ 1 := by rw [zero_add]; exact hgeom L

/- The averaging contradiction with weights: the progression starts `c + m + i + 1` need only be
coprime to `Q` for `m + i < p₀`; for the others the gcd's divisor count is at most `D ≤ 2^(p₀-m)`. -/
private lemma averaging_contra2 {f : ℕ → ℕ} (hfdd : ∀ n, f n ≤ dd n)
    {b m q Q c p₀ D : ℕ} (hb : 0 < b) (hQpos : 0 < Q) (hcQ : c < Q)
    (hQle : Q ≤ 2 ^ q) (hA2 : m + 3 * q ≤ 2 ^ q) (hA3 : 8 * b ≤ 2 ^ q)
    (hA4 : 4 * b * (3 + q) + 1 < 2 ^ m) (hmp : m ≤ p₀) (hD : D ≤ 2 ^ (p₀ - m))
    (hcop : ∀ i < 3 * q, m + i < p₀ → Nat.Coprime (c + m + i + 1) Q)
    (hgcd : ∀ i < 3 * q, dd (Nat.gcd (c + m + i + 1) Q) ≤ D)
    (hlow : ∀ t, (2 : ℝ) ^ m ≤ Tail f b (c + t * Q + m)) : False := by
  have hf : ∀ n, f n ≤ n := fun n => (hfdd n).trans (Nat.card_divisors_le_self n)
  set L := 3 * q with hLdef
  set X := Q + m + L with hXdef
  have hX1 : 1 ≤ X := by omega
  have hXpow : X ≤ 2 ^ (q + 1) := by rw [pow_succ]; omega
  have hLX : 2 * b * X ^ 2 ≤ 2 ^ L := by
    calc 2 * b * X ^ 2 ≤ 2 * b * (2 ^ (q + 1)) ^ 2 := by gcongr
      _ = 8 * b * (2 ^ q * 2 ^ q) := by ring
      _ ≤ 2 ^ q * (2 ^ q * 2 ^ q) := by gcongr
      _ = 2 ^ L := by rw [hLdef]; ring
  have hrange : ∀ t < X, c + t * Q < X * Q := by
    intro t ht
    have : (t + 1) * Q ≤ X * Q := Nat.mul_le_mul_right _ ht
    nlinarith
  have hXX : X * Q + m + L ≤ X * X := by
    have : X * X = X * Q + X * (m + L) := by rw [hXdef]; ring
    have : m + L ≤ X * (m + L) := Nat.le_mul_of_pos_left _ hX1
    omega
  have hupt : ∀ t < X, Tail f b (c + t * Q + m) ≤
      b * ∑ i ∈ Finset.range L, (f (c + m + i + 1 + t * Q) : ℝ) / 2 ^ (i + 1)
        + b * ((2 * X ^ 2 : ℕ) / 2 ^ L : ℝ) := by
    intro t ht
    have h := tail_upper hf b (c + t * Q + m) L
    have e : ∀ i, c + t * Q + m + i + 1 = c + m + i + 1 + t * Q := fun i => by ring
    simp only [e] at h
    refine h.trans (add_le_add le_rfl ?_)
    gcongr
    have := hrange t ht
    have h2 : c + t * Q + m + L + 2 ≤ 2 * X ^ 2 := by nlinarith
    exact_mod_cast h2
  set B : ℝ := 2 * X * (2 + Real.log X) with hBdef
  have hB0 : 0 ≤ B := by
    have : 0 ≤ Real.log X := Real.log_nonneg (by exact_mod_cast hX1)
    positivity
  -- the weight of position `i`
  set w : ℕ → ℝ := fun i => if m + i < p₀ then 1 else D with hw
  have hF : ∀ i ∈ Finset.range L, (∑ t ∈ Finset.range X, (f (c + m + i + 1 + t * Q) : ℝ)) ≤ w i * B := by
    intro i hi
    have hiL : i < L := by simpa using hi
    have hXi : ∀ t < X, c + m + i + 1 + t * Q ≤ X * X := by
      intro t ht
      have := hrange t ht
      omega
    calc (∑ t ∈ Finset.range X, (f (c + m + i + 1 + t * Q) : ℝ))
        ≤ ∑ t ∈ Finset.range X, (dd (c + m + i + 1 + t * Q) : ℝ) :=
          Finset.sum_le_sum fun t _ => by exact_mod_cast hfdd (c + m + i + 1 + t * Q)
      _ ≤ w i * B := by
          simp only [hw]
          split_ifs with hip
          · rw [one_mul]
            exact sum_dd_AP_le _ _ _ (hcop i hiL hip) hXi
          · calc (∑ t ∈ Finset.range X, (dd (c + m + i + 1 + t * Q) : ℝ))
                ≤ dd (Nat.gcd (c + m + i + 1) Q) * B := sum_dd_AP_le' _ _ _ hQpos hXi
              _ ≤ D * B := by gcongr; exact_mod_cast hgcd i hiL
  -- the weighted geometric sum is at most 2
  have hwsum : ∑ i ∈ Finset.range L, w i * (1 / 2 : ℝ) ^ (i + 1) ≤ 2 := by
    have hgeom : ∀ L : ℕ, ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1) ≤ 1 := by
      intro L
      have : ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1) = 1 - (1 / 2) ^ L := by
        induction L with
        | zero => simp
        | succ n ih => rw [Finset.sum_range_succ, ih]; ring
      rw [this]; linarith [pow_pos (by norm_num : (0 : ℝ) < 1 / 2) L]
    have hterm : ∀ i, w i * (1 / 2 : ℝ) ^ (i + 1) ≤
        (1 / 2 : ℝ) ^ (i + 1) + (if p₀ - m ≤ i then (1 / 2 : ℝ) ^ (i + 1 - (p₀ - m)) else 0) := by
      intro i
      simp only [hw]
      split_ifs with h1 h2
      · rw [one_mul]; linarith [pow_pos (by norm_num : (0 : ℝ) < 1 / 2) (i + 1 - (p₀ - m))]
      · rw [one_mul, add_zero]
      · have hD' : (D : ℝ) ≤ 2 ^ (p₀ - m) := by exact_mod_cast hD
        have hpow : (1 / 2 : ℝ) ^ (i + 1) =
            (1 / 2 : ℝ) ^ (i + 1 - (p₀ - m)) * (1 / 2 : ℝ) ^ (p₀ - m) := by
          rw [← pow_add]; congr 1; omega
        have hDb : (D : ℝ) * (1 / 2 : ℝ) ^ (p₀ - m) ≤ 1 := by
          rw [one_div_pow, mul_one_div, div_le_one (by positivity)]; exact hD'
        have ha : (0 : ℝ) ≤ (1 / 2 : ℝ) ^ (i + 1 - (p₀ - m)) := by positivity
        calc (D : ℝ) * (1 / 2 : ℝ) ^ (i + 1)
            = (1 / 2 : ℝ) ^ (i + 1 - (p₀ - m)) * ((D : ℝ) * (1 / 2 : ℝ) ^ (p₀ - m)) := by
              rw [hpow]; ring
          _ ≤ (1 / 2 : ℝ) ^ (i + 1 - (p₀ - m)) * 1 := by gcongr
          _ ≤ (1 / 2 : ℝ) ^ (i + 1) + (1 / 2 : ℝ) ^ (i + 1 - (p₀ - m)) := by
              rw [mul_one]; linarith [pow_pos (by norm_num : (0 : ℝ) < 1 / 2) (i + 1)]
      · omega
    calc ∑ i ∈ Finset.range L, w i * (1 / 2 : ℝ) ^ (i + 1)
        ≤ ∑ i ∈ Finset.range L, ((1 / 2 : ℝ) ^ (i + 1)
            + (if p₀ - m ≤ i then (1 / 2 : ℝ) ^ (i + 1 - (p₀ - m)) else 0)) :=
          Finset.sum_le_sum fun i _ => hterm i
      _ = ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1)
            + ∑ i ∈ Finset.range L, (if p₀ - m ≤ i then (1 / 2 : ℝ) ^ (i + 1 - (p₀ - m)) else 0) :=
          Finset.sum_add_distrib
      _ ≤ 1 + 1 := add_le_add (hgeom L) (geom_tail_le _ _)
      _ = 2 := by norm_num
  have hmain : (X : ℝ) * 2 ^ m ≤ b * (2 * B) + X := by
    calc (X : ℝ) * 2 ^ m = ∑ t ∈ Finset.range X, (2 : ℝ) ^ m := by simp
      _ ≤ ∑ t ∈ Finset.range X, Tail f b (c + t * Q + m) := Finset.sum_le_sum fun t _ => hlow t
      _ ≤ ∑ t ∈ Finset.range X, (b * ∑ i ∈ Finset.range L, (f (c + m + i + 1 + t * Q) : ℝ) / 2 ^ (i + 1)
            + b * ((2 * X ^ 2 : ℕ) / 2 ^ L : ℝ)) :=
          Finset.sum_le_sum fun t ht => hupt t (by simpa using ht)
      _ = b * ∑ i ∈ Finset.range L, (∑ t ∈ Finset.range X, (f (c + m + i + 1 + t * Q) : ℝ)) * (1 / 2) ^ (i + 1)
            + X * (b * ((2 * X ^ 2 : ℕ) / 2 ^ L : ℝ)) := by
          rw [Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_comm]
          simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul, Finset.sum_mul, div_eq_mul_inv,
            inv_pow, one_mul]
      _ ≤ b * ∑ i ∈ Finset.range L, (w i * B) * (1 / 2) ^ (i + 1) + X * 1 := by
          apply add_le_add
          · apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
            apply Finset.sum_le_sum
            intro i hi
            exact mul_le_mul_of_nonneg_right (hF i hi) (by positivity)
          · apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
            rw [← mul_div_assoc, div_le_one (by positivity)]
            have h1 : b * (2 * X ^ 2) ≤ 2 ^ L := by
              calc b * (2 * X ^ 2) = 2 * b * X ^ 2 := by ring
                _ ≤ 2 ^ L := hLX
            exact_mod_cast h1
      _ ≤ b * (2 * B) + X := by
          rw [mul_one]
          apply add_le_add_left
          apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
          calc ∑ i ∈ Finset.range L, (w i * B) * (1 / 2 : ℝ) ^ (i + 1)
              = B * ∑ i ∈ Finset.range L, w i * (1 / 2 : ℝ) ^ (i + 1) := by
                rw [Finset.mul_sum]; apply Finset.sum_congr rfl; intro i _; ring
            _ ≤ B * 2 := mul_le_mul_of_nonneg_left hwsum hB0
            _ = 2 * B := mul_comm _ _
  have hXpos : (0 : ℝ) < X := by exact_mod_cast hX1
  have h2m : (2 : ℝ) ^ m ≤ 4 * b * (2 + Real.log X) + 1 := by
    have : (X : ℝ) * 2 ^ m ≤ X * (4 * b * (2 + Real.log X) + 1) := by
      rw [hBdef] at hmain; nlinarith
    exact le_of_mul_le_mul_left this hXpos
  have hlogX : Real.log X ≤ q + 1 := by
    calc Real.log X ≤ Real.log ((2 : ℝ) ^ (q + 1)) :=
          Real.log_le_log hXpos (by exact_mod_cast hXpow)
      _ = (q + 1) * Real.log 2 := by rw [Real.log_pow]; push_cast; ring
      _ ≤ (q + 1) * 1 := by
          gcongr
          linarith [Real.log_two_lt_d9]
      _ = q + 1 := mul_one _
  have hA4' : (4 * b * (3 + q) + 1 : ℝ) < 2 ^ m := by exact_mod_cast hA4
  have : (4 * b * (2 + Real.log X) + 1 : ℝ) ≤ 4 * b * (3 + q) + 1 := by
    have : (0 : ℝ) ≤ b := by positivity
    nlinarith
  linarith

/- The divisor count of a product of squares of distinct primes. -/
private lemma dd_prod_sq {ι : Type*} (S : Finset ι) (pr : ι → ℕ) (hp : ∀ i ∈ S, (pr i).Prime)
    (hinj : Set.InjOn pr (S : Set ι)) : dd (∏ i ∈ S, pr i ^ 2) = 3 ^ S.card := by
  classical
  induction S using Finset.induction_on with
  | empty => simp [dd]
  | insert a S haS ih =>
    rw [Finset.prod_insert haS, Finset.card_insert_of_notMem haS, pow_succ (3 : ℕ) S.card]
    have hpa := hp a (Finset.mem_insert_self _ _)
    have hcop : Nat.Coprime (pr a ^ 2) (∏ i ∈ S, pr i ^ 2) := by
      apply Nat.Coprime.prod_right
      intro i hi
      apply Nat.Coprime.pow
      rw [Nat.coprime_primes hpa (hp i (Finset.mem_insert_of_mem hi))]
      intro h
      exact haS (hinj (Finset.mem_insert_self _ _) (Finset.mem_insert_of_mem hi) h ▸ hi)
    unfold dd
    rw [Nat.Coprime.card_divisors_mul hcop]
    have h3 : (pr a ^ 2).divisors.card = 3 := by
      rw [Nat.divisors_prime_pow hpa 2, Finset.card_map, Finset.card_range]
    rw [h3]
    have ih' := ih (fun i hi => hp i (Finset.mem_insert_of_mem hi))
      (hinj.mono (by simp))
    unfold dd at ih'
    rw [ih', mul_comm]

private lemma eight_mul_le_two_pow {q : ℕ} (hq : 6 ≤ q) : 8 * q ≤ 2 ^ q := by
  induction q with
  | zero => omega
  | succ n ih =>
    rcases Nat.lt_or_ge n 6 with h | h
    · interval_cases n <;> first | omega | norm_num
    · have := ih h
      rw [pow_succ]; omega

private lemma exists_param2 (b P : ℕ) :
    ∃ m : ℕ, b ≤ m ∧ 1 ≤ m ∧ 4 * m * (3 + 2000 * P ^ 3 * m ^ 12) + 1 < 2 ^ m := by
  have h := tendsto_pow_const_div_const_pow_of_one_lt 13 (r := (2:ℝ)) (by norm_num)
  have hC : (0 : ℝ) < 1 / (13 + 8000 * (P : ℝ) ^ 3) := by positivity
  have h2 := (h.eventually (gt_mem_nhds hC)).and (Filter.eventually_ge_atTop (max b 1))
  obtain ⟨m, hm, hmb⟩ := h2.exists
  refine ⟨m, le_of_max_le_left hmb, le_of_max_le_right hmb, ?_⟩
  have hm1 : (1 : ℝ) ≤ m := by exact_mod_cast le_of_max_le_right hmb
  have h13 : (m : ℝ) ^ 13 < 1 / (13 + 8000 * (P : ℝ) ^ 3) * 2 ^ m := by
    rwa [div_lt_iff₀ (by positivity)] at hm
  have hpos : (0 : ℝ) < 13 + 8000 * (P : ℝ) ^ 3 := by positivity
  have hkey : (13 + 8000 * (P : ℝ) ^ 3) * (m : ℝ) ^ 13 < 2 ^ m := by
    rw [div_mul_eq_mul_div, one_mul, lt_div_iff₀ hpos] at h13
    linarith
  have hle : (4 * m * (3 + 2000 * P ^ 3 * m ^ 12) + 1 : ℝ) ≤ (13 + 8000 * (P : ℝ) ^ 3) * (m : ℝ) ^ 13 := by
    have hm13 : (m : ℝ) ≤ (m : ℝ) ^ 13 := le_self_pow₀ hm1 (by norm_num)
    have h1 : (1 : ℝ) ≤ (m : ℝ) ^ 13 := one_le_pow₀ hm1
    have hP0 : (0 : ℝ) ≤ (P : ℝ) ^ 3 := by positivity
    nlinarith
  have : (4 * m * (3 + 2000 * P ^ 3 * m ^ 12) + 1 : ℝ) < 2 ^ m := lt_of_le_of_lt hle hkey
  exact_mod_cast this


theorem variant_5274cf38__h1 : ∀ (B : Set ℕ),
  B.Nonempty →
    (∃ (p : ℕ), (0 : ℕ) < p ∧ ∀ (n : ℕ), n ∈ B ↔ n + p ∈ B) →
      Irrational (∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ))) := by
  -- approach: Erdős 1948 with f_B(m) = #{d | m : d ∈ B}, as in the partial already on this node, but the averaging absorbs the small primes by their tail weight 2^(-i), so the prime supply needed is only m² primes ≡ 1 mod P above 2m²+m with product ≤ 2^(1000P³m¹²), provable from Mathlib by cyclotomic polynomials
  -- licence: CC-BY-4.0
  -- label: m² primes ≡ 1 mod P, product at most 2^(1000 P³ m¹²)
  -- claim: $\forall P \ge 1\ \forall m \ge 1\ \exists S \subseteq \mathbb{P},\ |S| = m^2,\ \forall p \in S:\ p \equiv 1 \pmod P,\ p > 2m^2 + m,\ \text{and } \prod_{p \in S} p \le 2^{1000 P^3 m^{12}}$
  -- Provable from the pinned Mathlib: with n = 6Pm² (not a prime power) and b_s = 1 + n·B₀!·s, every prime factor of Φ_n(b_s) is ≡ 1 (mod n) and exceeds B₀ (Φ_n(b_s) ≡ Φ_n(1) = 1 modulo every prime ≤ B₀), and lies below b_s^n; the b_s are distinct roots of X^n − 1 modulo such a prime, so B₀ = n·m² values of s give m² distinct primes (Polynomial.isRoot_cyclotomic_iff, eval_one_cyclotomic_not_prime_pow, card_nthRoots).
  have hprimes : ∀ P : ℕ, 0 < P → ∀ m : ℕ, 1 ≤ m → ∃ S : Finset ℕ, S.card = m * m ∧
      (∀ p ∈ S, p.Prime ∧ p % P = 1 ∧ 2 * m * m + m < p) ∧
      ∏ p ∈ S, p ≤ 2 ^ (1000 * P ^ 3 * m ^ 12) := by
    sorry
  intro B hB ⟨P, hP, hper⟩
  classical
  obtain ⟨r, hr⟩ := hB
  have hfle : ∀ n, fB B n ≤ n := fB_le B
  have hfdd : ∀ n, fB B n ≤ dd n := fB_le_dd B
  have hposB : ∀ j, ∃ i, 0 < fB B (j + i + 1) := by
    intro j
    obtain ⟨i, hi⟩ := exists_mem_gt hP hper hr j
    exact ⟨i, fB_pos B (by omega) hi⟩
  rw [lambert_set B]
  rintro ⟨qr, hq⟩
  set a : ℤ := qr.num
  set b : ℕ := qr.den
  have hb : 0 < b := qr.pos
  have hx : ∑' n : ℕ, (fB B n : ℝ) / 2 ^ n = a / b := by
    rw [← hq]; exact Rat.cast_def qr
  have hT : ∀ j, Tail (fB B) b j = Zint (fB B) a b j := tail_eq_Zint hfle hb hx
  obtain ⟨m, hbm, hm1, hA4m⟩ := exists_param2 b P
  set q := 2000 * P ^ 3 * m ^ 12 with hqdef
  have hP3 : 1 ≤ P ^ 3 := Nat.one_le_pow _ _ hP
  have hm12 : m ≤ m ^ 12 := le_self_pow₀ hm1 (by norm_num)
  have hq6 : 6 ≤ q := by
    have : 1 ≤ P ^ 3 * m ^ 12 := Nat.one_le_iff_ne_zero.mpr (by positivity)
    simp only [hqdef]; nlinarith
  have hmq : m ≤ q := by
    simp only [hqdef]
    calc m ≤ m ^ 12 := hm12
      _ ≤ 2000 * P ^ 3 * m ^ 12 := by nlinarith
  have h8q : 8 * q ≤ 2 ^ q := eight_mul_le_two_pow hq6
  have hA2 : m + 3 * q ≤ 2 ^ q := by omega
  have hA3 : 8 * b ≤ 2 ^ q := by
    have : 8 * b ≤ 8 * q := by omega
    omega
  have hA4 : 4 * b * (3 + q) + 1 < 2 ^ m := by
    calc 4 * b * (3 + q) + 1 ≤ 4 * m * (3 + q) + 1 := by gcongr
      _ < 2 ^ m := hA4m
  set p₀ := 2 * m * m + m + 1 with hp₀def
  have hmp : m ≤ p₀ := by omega
  obtain ⟨T, hTcard, hTp, hTprod⟩ := hprimes P hP m hm1
  set S : Finset (ℕ × ℕ) := Finset.range m ×ˢ Finset.range m with hSdef
  have hmemS : ∀ ij ∈ S, ij.1 * m + ij.2 < m * m := by
    intro ij hij
    simp only [hSdef, Finset.mem_product, Finset.mem_range] at hij
    nlinarith
  -- the primes, indexed by position `i` and slot `j`
  obtain ⟨pr, hprp, hprT, hinj⟩ : ∃ pr : ℕ × ℕ → ℕ, (∀ ij, (pr ij).Prime) ∧
      (∀ ij ∈ S, pr ij ∈ T) ∧ Set.InjOn pr (S : Set (ℕ × ℕ)) := by
    refine ⟨fun ij => if h : ij.1 * m + ij.2 < m * m then T.orderEmbOfFin hTcard ⟨_, h⟩ else 2,
      ?_, ?_, ?_⟩
    · intro ij
      dsimp only
      split_ifs with h
      · exact (hTp _ (Finset.orderEmbOfFin_mem T hTcard _)).1
      · exact Nat.prime_two
    · intro ij hij
      dsimp only
      rw [dif_pos (hmemS ij hij)]
      exact Finset.orderEmbOfFin_mem T hTcard _
    · intro x hx y hy hxy
      have hx' := hmemS x hx
      have hy' := hmemS y hy
      dsimp only at hxy
      rw [dif_pos hx', dif_pos hy'] at hxy
      have h1 : x.1 * m + x.2 = y.1 * m + y.2 := by
        have := (T.orderEmbOfFin hTcard).injective hxy
        simpa using this
      simp only [hSdef, Finset.coe_product, Finset.coe_range, Set.mem_prod, Set.mem_Iio] at hx hy
      obtain ⟨e1, e2⟩ := idx_inj hx.2 hy.2 h1
      exact Prod.ext e1 e2
  have hprlo : ∀ ij ∈ S, 2 * m * m + m < pr ij := fun ij hij => (hTp _ (hprT ij hij)).2.2
  have hprmod : ∀ ij ∈ S, pr ij % P = 1 := fun ij hij => (hTp _ (hprT ij hij)).2.1
  set Q : ℕ := ∏ ij ∈ S, pr ij ^ 2 with hQdef
  have hQpos : 0 < Q := Finset.prod_pos (fun ij _ => pow_pos (hprp ij).pos 2)
  have hScard : S.card = m * m := by
    rw [hSdef, Finset.card_product, Finset.card_range]
  have hprodle : ∏ ij ∈ S, pr ij ≤ ∏ p ∈ T, p := by
    have himg : ∏ p ∈ S.image pr, p = ∏ ij ∈ S, pr ij :=
      Finset.prod_image (fun x hx y hy h => hinj hx hy h)
    rw [← himg]
    exact Finset.prod_le_prod_of_subset_of_one_le' (Finset.image_subset_iff.mpr hprT)
      (fun p hp _ => (hTp p hp).1.one_lt.le)
  have hQle : Q ≤ 2 ^ q := by
    calc Q = (∏ ij ∈ S, pr ij) ^ 2 := by rw [hQdef, Finset.prod_pow]
      _ ≤ (2 ^ (1000 * P ^ 3 * m ^ 12)) ^ 2 := by gcongr; exact hprodle.trans hTprod
      _ = 2 ^ q := by rw [← pow_mul, hqdef]; ring_nf
  have hD : dd Q ≤ 2 ^ (p₀ - m) := by
    rw [hQdef, dd_prod_sq S pr (fun ij _ => hprp ij) hinj, hScard]
    calc 3 ^ (m * m) ≤ 4 ^ (m * m) := Nat.pow_le_pow_left (by norm_num) _
      _ = 2 ^ (2 * (m * m)) := by rw [pow_mul (2 : ℕ) 2 (m * m)]; norm_num
      _ ≤ 2 ^ (p₀ - m) := by
          apply Nat.pow_le_pow_right (by norm_num)
          have e2 : 2 * m * m = 2 * (m * m) := by ring
          rw [hp₀def]
          omega
  set L := 3 * q with hLdef
  have hdvdQ : ∀ ij ∈ S, pr ij ^ 2 ∣ Q := fun ij hij => Finset.dvd_prod_of_mem _ hij
  -- Chinese remainder theorem
  have hs : ∀ ij ∈ S, pr ij ^ 2 ≠ 0 := fun ij _ => (pow_pos (hprp ij).pos 2).ne'
  have pp : Set.Pairwise (S : Set (ℕ × ℕ)) (Function.onFun Nat.Coprime fun ij => pr ij ^ 2) := by
    intro x hx y hy hxy
    exact Nat.Coprime.pow 2 2 ((Nat.coprime_primes (hprp x) (hprp y)).2
      (fun h => hxy (hinj hx hy h)))
  set crt := Nat.chineseRemainderOfFinset (fun ij => pr ij ^ 2 + pr ij - (ij.1 + 1))
    (fun ij => pr ij ^ 2) S hs pp
  set c : ℕ := crt.1
  have hc : ∀ ij ∈ S, c ≡ pr ij ^ 2 + pr ij - (ij.1 + 1) [MOD pr ij ^ 2] := crt.2
  have hcQ : c < Q := Nat.chineseRemainderOfFinset_lt_prod _ _ hs pp
  -- the key congruence
  have hk : ∀ t, ∀ ij ∈ S, c + t * Q + (ij.1 + 1) ≡ pr ij [MOD pr ij ^ 2] := by
    intro t ij hij
    obtain ⟨R, hR⟩ := hdvdQ ij hij
    have hi : ij.1 < m := by
      simp only [hSdef, Finset.mem_product, Finset.mem_range] at hij; exact hij.1
    have hp := hprlo ij hij
    have e1 : c + t * Q ≡ c [MOD pr ij ^ 2] := by
      rw [hR, show t * (pr ij ^ 2 * R) = pr ij ^ 2 * (t * R) by ring]
      exact Nat.add_mul_mod_self_left _ _ _
    have e2 := (e1.trans (hc ij hij)).add_right (ij.1 + 1)
    rw [Nat.sub_add_cancel (by nlinarith)] at e2
    refine e2.trans ?_
    exact Nat.add_mod_left _ _
  -- forced divisibility
  have hforced : ∀ t, ∀ n, c + t * Q < n → n ≤ c + t * Q + m → 2 ^ m ∣ fB B n := by
    intro t n hn1 hn2
    obtain ⟨i, rfl⟩ : ∃ i, n = c + t * Q + (i + 1) := ⟨n - (c + t * Q) - 1, by omega⟩
    have hi : i < m := by omega
    have hcard : ((Finset.range m).image (fun j => pr (i, j))).card = m := by
      rw [Finset.card_image_of_injOn, Finset.card_range]
      intro j hj j' hj' h
      have := hinj (by simp [hSdef, hi, (by simpa using hj : j < m)])
        (by simp [hSdef, hi, (by simpa using hj' : j' < m)]) h
      simpa using this
    rw [← hcard]
    apply pow_two_dvd_fB B hP hper _ _ (by omega)
    intro p hp
    obtain ⟨j, hj, rfl⟩ := Finset.mem_image.mp hp
    have hij : (i, j) ∈ S := by simp [hSdef, hi, (by simpa using hj : j < m)]
    have h := hk t (i, j) hij
    have hpp := hprp (i, j)
    refine ⟨hpp, hprmod _ hij, (h.dvd_iff (Dvd.intro_left _ (pow_two _).symm)).2 dvd_rfl, ?_⟩
    rw [h.dvd_iff dvd_rfl]
    intro hd
    have := Nat.le_of_dvd hpp.pos hd
    have := hpp.two_le
    nlinarith
  -- coprimality for the positions below the smallest prime
  have hcop : ∀ i < L, m + i < p₀ → Nat.Coprime (c + m + i + 1) Q := by
    intro i hi hip
    apply Nat.Coprime.prod_right
    intro ij hij
    apply Nat.Coprime.pow_right
    rw [Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd (hprp ij)]
    intro hd
    have hi0 : ij.1 < m := by
      simp only [hSdef, Finset.mem_product, Finset.mem_range] at hij; exact hij.1
    have h1 : pr ij ∣ c + 0 * Q + (ij.1 + 1) :=
      ((hk 0 ij hij).dvd_iff (Dvd.intro_left _ (pow_two _).symm)).2 dvd_rfl
    have h2 : c + m + i + 1 = (c + 0 * Q + (ij.1 + 1)) + (m + i - ij.1) := by omega
    rw [h2] at hd
    have h3 := (Nat.dvd_add_right h1).mp hd
    have h4 := Nat.le_of_dvd (by omega) h3
    have := hprlo ij hij
    omega
  have hgcd : ∀ i < L, dd (Nat.gcd (c + m + i + 1) Q) ≤ dd Q :=
    fun i _ => dd_le_of_dvd hQpos.ne' (Nat.gcd_dvd_right _ _)
  -- lower bound
  have hlow : ∀ t, (2 : ℝ) ^ m ≤ Tail (fB B) b (c + t * Q + m) := by
    intro t
    have hd := Zint_dvd (fB B) a b (c + t * Q) m (hforced t)
    obtain ⟨i₀, hi₀⟩ := hposB (c + t * Q + m)
    have hpos := tail_pos hfle hb (c + t * Q + m) hi₀
    rw [hT] at hpos ⊢
    have hpos' : 0 < Zint (fB B) a b (c + t * Q + m) := by exact_mod_cast hpos
    have := Int.le_of_dvd hpos' hd
    exact_mod_cast this
  exact averaging_contra2 hfdd hb hQpos hcQ hQle hA2 hA3 hA4 hmp hD hcop hgcd hlow