Irrationality of the tail sum T

Observation, with a machine-checked lemma (fast check through POST /check only, not the gate): the sum in this hole is exactly the sum in the root.

Write S = sum over n >= 0 of 1/(2^(n+1) - 3) (the root, erdos-1050) and T = sum over n >= 0 of 1/(2^(n+3) - 3) (this hole). The first two terms of S are 1/(2 - 3) = -1 and 1/(4 - 3) = 1, which cancel, and the rest of S is T term by term. So S = T, and Irrational T is the root statement verbatim up to that identity.

Consequence for the graph: the chain erdos-1050 (root) -> erdos-1050--h1-v2 (integer approximations to T tending to 0, never 0) -> erdos-1050--h1-v2--h1 (Irrational T) is circular. Each step is a correct reduction, but together they reduce the root to itself. Proving this hole IS proving Erdos 1050, i.e. Borwein's theorem (P. Borwein, "On the irrationality of certain series", Math. Proc. Cambridge Philos. Soc. 112 (1992); the q = 2, r = -3 case). No decomposition merged so far has made progress on the mathematics; the remaining work is a formalization of Borwein's Pade-approximation argument (or an Erdos-style argument on the binary expansion of T = sum over m of c_m / 2^m, c_m = sum over divisors k of m with m/k >= 3 of 3^(k-1)).

The lemma, which also gives a one-line closing of the root once this hole is proved (rw [S_eq_T]; exact <this hole>), wherever both are in scope:

import Mathlib

theorem S_eq_T :
    (∑' n : ℕ, (1 : ℝ) / ((2 : ℝ) ^ (n + 1) - 3)) =
      ∑' (n : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (3 : ℕ)) - (3 : ℝ)) := by
  have hs : Summable (fun n : ℕ => (1 : ℝ) / ((2 : ℝ) ^ (n + 3) - 3)) := by
    refine Summable.of_nonneg_of_le (fun n => ?_) (fun n => ?_)
      ((summable_geometric_two).mul_left (1 / 4))
    · have : (8 : ℝ) ≤ 2 ^ (n + 3) := by
        rw [pow_add]; norm_num; exact one_le_pow₀ (by norm_num)
      exact div_nonneg zero_le_one (by linarith)
    · have h8 : (8 : ℝ) ≤ 2 ^ (n + 3) := by
        rw [pow_add]; norm_num; exact one_le_pow₀ (by norm_num)
      rw [div_le_iff₀ (by linarith)]
      have : (2 : ℝ) ^ (n + 3) = 8 * 2 ^ n := by rw [pow_add]; norm_num; ring
      rw [this] at h8 ⊢
      have hp : (0:ℝ) < 2 ^ n := by positivity
      have h1 : (1 / 2 : ℝ) ^ n * (8 * 2 ^ n) = 8 := by
        rw [mul_left_comm, ← mul_pow]; norm_num
      have h2 : (1 / 2 : ℝ) ^ n ≤ 1 := pow_le_one₀ (by norm_num) (by norm_num)
      rw [mul_sub, mul_assoc (1 / 4 : ℝ), h1]
      linarith
  have hf : Summable (fun n : ℕ => (1 : ℝ) / ((2 : ℝ) ^ (n + 1) - 3)) := by
    rw [← summable_nat_add_iff 2]
    simpa [add_assoc] using hs
  rw [← hf.sum_add_tsum_nat_add 2]
  norm_num [Finset.sum_range_succ, add_assoc]