Erdős problem 354 - part i

/- A proof of the full Erdős 354(levelIndex) proposition. -/


/- Source: DigitTransport.lean -/
section
namespace Erdos354Formal

/-- A predicate has occurrences arbitrarily far to the right. -/
def UnboundedOnes (A : ℕ → Prop) : Prop :=
  ∀ N, ∃ a, N ≤ a ∧ A a

/-- Each sufficiently late occurrence of `A` forces an occurrence of `B`
in an interval of fixed length starting `b` positions later. -/
def ForwardTransport (A B : ℕ → Prop) (b : ℕ) : Prop :=
  ∃ L, 0 < L ∧ ∃ N, ∀ a, N ≤ a → A a →
    ∃ y, a + b ≤ y ∧ y < a + b + L ∧ B y

/-- Every interval of one fixed positive length contains an occurrence. -/
def BoundedZeroRuns (A : ℕ → Prop) : Prop :=
  ∃ H, 0 < H ∧ ∀ n, ∃ y, n ≤ y ∧ y < n + H ∧ A y

theorem ForwardTransport.unbounded {A B : ℕ → Prop} {b : ℕ}
    (h : ForwardTransport A B b) (hA : UnboundedOnes A) : UnboundedOnes B := by
  obtain ⟨L, _, N, h⟩ := h
  intro t
  obtain ⟨a, ha, hAa⟩ := hA (max t N)
  obtain ⟨y, hay, _, hBy⟩ := h a (by omega) hAa
  exact ⟨y, by omega, hBy⟩

theorem ForwardTransport.compose {A B C : ℕ → Prop} {b d : ℕ}
    (hAB : ForwardTransport A B b) (hBC : ForwardTransport B C d) :
    ForwardTransport A C (b + d) := by
  obtain ⟨L, hL, N, hAB⟩ := hAB
  obtain ⟨M, hM, K, hBC⟩ := hBC
  refine ⟨L + M, by omega, max N K, ?_⟩
  intro a ha hAa
  obtain ⟨y, hay, hya, hBy⟩ := hAB a (by omega) hAa
  obtain ⟨z, hyz, hzy, hCz⟩ := hBC y (by omega) hBy
  exact ⟨z, by omega, by omega, hCz⟩

/-- A strictly forward return of bounded length rules out unbounded gaps. -/
theorem boundedZeroRuns_of_forward_return {A : ℕ → Prop} {b : ℕ}
    (hb : 0 < b) (hA : UnboundedOnes A) (h : ForwardTransport A A b) :
    BoundedZeroRuns A := by
  obtain ⟨L, hL, N, h⟩ := h
  obtain ⟨a₀, ha₀N, hAa₀⟩ := hA N
  let H := a₀ + b + L + 1
  have hH : 0 < H := by dsimp [H]; omega
  have hall : ∀ n, ∃ y, N ≤ y ∧ n ≤ y ∧ y < n + H ∧ A y := by
    intro n
    induction n with
    | zero =>
      exact ⟨a₀, ha₀N, Nat.zero_le _, by dsimp [H]; omega, hAa₀⟩
    | succ n ih =>
      obtain ⟨y, hNy, hny, hyH, hAy⟩ := ih
      by_cases hn : n + 1 ≤ y
      · exact ⟨y, hNy, hn, by omega, hAy⟩
      · have hy : y = n := by omega
        subst y
        obtain ⟨z, hnz, hzn, hAz⟩ := h n hNy hAy
        exact ⟨z, by omega, by omega, by dsimp [H] at *; omega, hAz⟩
  refine ⟨H, hH, ?_⟩
  intro n
  obtain ⟨y, _, hny, hyH, hAy⟩ := hall n
  exact ⟨y, hny, hyH, hAy⟩

/-- The final digit argument from the proposed mathematical proof. -/
theorem boundedZeroRuns_of_two_transports {A B : ℕ → Prop} {b d : ℕ}
    (hb : 0 < b) (hd : 0 < d) (hA : UnboundedOnes A)
    (hAB : ForwardTransport A B b) (hBA : ForwardTransport B A d) :
    BoundedZeroRuns A :=
  boundedZeroRuns_of_forward_return (by omega) hA (hAB.compose hBA)

end Erdos354Formal
end


/- Source: BinaryFloors.lean -/
section
/- Binary floor heights and the elementary arithmetic part of Erdős 354. -/

namespace Erdos354Formal

noncomputable def height (α : ℝ) (n : ℕ) : ℤ :=
  Erdos354.FloorMultiples α 2 n

noncomputable def digit (α : ℝ) (n : ℕ) : ℤ :=
  height α (n + 1) - 2 * height α n

def Dyadic (α : ℝ) : Prop := ∃ n : ℕ, ∃ z : ℤ, α = z / (2 : ℝ) ^ n

def Ones (α : ℝ) (n : ℕ) : Prop := digit α n = 1

theorem digit_zero_or_one (α : ℝ) (n : ℕ) : digit α n = 0 ∨ digit α n = 1 := by
  have hlo := Int.le_floor_add ((2 : ℝ) ^ n * α) ((2 : ℝ) ^ n * α)
  have hhi := Int.le_floor_add_floor ((2 : ℝ) ^ n * α) ((2 : ℝ) ^ n * α)
  have heq : (2 : ℝ) ^ (n + 1) * α = 2 ^ n * α + 2 ^ n * α := by
    rw [pow_succ]
    ring
  simp only [digit, height, Erdos354.FloorMultiples, heq]
  omega

theorem height_recurrence (α : ℝ) (n : ℕ) :
    height α (n + 1) = 2 * height α n + digit α n := by
  dsimp [digit]
  ring

theorem digit_nonneg (α : ℝ) (n : ℕ) : 0 ≤ digit α n := by
  rcases digit_zero_or_one α n with h | h <;> omega

theorem digit_le_one (α : ℝ) (n : ℕ) : digit α n ≤ 1 := by
  rcases digit_zero_or_one α n with h | h <;> omega

theorem height_positive {α : ℝ} (hα : 1 ≤ α) (n : ℕ) : 0 < height α n := by
  have hpow : (1 : ℝ) ≤ 2 ^ n := one_le_pow₀ (by norm_num)
  have hh : (1 : ℝ) ≤ 2 ^ n * α := by
    nlinarith [mul_nonneg (sub_nonneg.mpr hpow) (sub_nonneg.mpr hα)]
  have : (1 : ℤ) ≤ height α n := by
    apply Int.le_floor.mpr
    simpa using hh
  omega

theorem height_sum_gap (α : ℝ) (n : ℕ) :
    height α n - ∑ levelIndex ∈ Finset.range n, height α levelIndex =
      height α 0 + ∑ levelIndex ∈ Finset.range n, digit α levelIndex := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [Finset.sum_range_succ, Finset.sum_range_succ, height_recurrence]
    linarith

theorem sum_height_lt {α : ℝ} (hα : 1 ≤ α) (n : ℕ) :
    (∑ levelIndex ∈ Finset.range n, height α levelIndex) < height α n := by
  have hsum : 0 ≤ ∑ levelIndex ∈ Finset.range n, digit α levelIndex :=
    Finset.sum_nonneg fun levelIndex _ => digit_nonneg α levelIndex
  have := height_sum_gap α n
  have := height_positive hα 0
  omega

theorem height_tail_zero {α : ℝ} {N : ℕ}
    (h : ∀ n, N ≤ n → digit α n = 0) (k : ℕ) :
    height α (N + k) = (2 : ℤ) ^ k * height α N := by
  induction k with
  | zero => simp
  | succ k ih =>
    rw [Nat.add_succ, height_recurrence, h (N + k) (by omega), ih, pow_succ]
    ring

theorem dyadic_of_eventually_zero {α : ℝ} {N : ℕ}
    (h : ∀ n, N ≤ n → digit α n = 0) : Dyadic α := by
  let x : ℝ := (2 : ℝ) ^ N * α
  let z : ℤ := height α N
  have hz : (z : ℝ) ≤ x := Int.floor_le x
  have hupper : ∀ k : ℕ, (2 : ℝ) ^ k * (x - z) < 1 := by
    intro k
    have heq := height_tail_zero h k
    have hfloor := Int.lt_floor_add_one ((2 : ℝ) ^ (N + k) * α)
    change _ < (height α (N + k) : ℝ) + 1 at hfloor
    rw [heq] at hfloor
    push_cast at hfloor
    dsimp [x, z]
    rw [pow_add] at hfloor
    nlinarith
  have heq : x = z := by
    by_contra hne
    have hpos : 0 < x - z := sub_pos.mpr (lt_of_le_of_ne hz (Ne.symm hne))
    obtain ⟨k, hkn⟩ := exists_nat_gt (1 / (x - z))
    have hkpow : (k : ℝ) < (2 : ℝ) ^ k := by exact_mod_cast Nat.lt_two_pow_self
    have hk := lt_trans hkn hkpow
    have hlarge : 1 < (2 : ℝ) ^ k * (x - z) := (div_lt_iff₀ hpos).mp hk
    exact (not_lt_of_gt hlarge) (hupper k)
  refine ⟨N, z, ?_⟩
  apply (eq_div_iff (by positivity : (2 : ℝ) ^ N ≠ 0)).mpr
  dsimp [x] at heq
  nlinarith

theorem unboundedOnes_of_not_dyadic {α : ℝ} (hα : ¬ Dyadic α) :
    UnboundedOnes (Ones α) := by
  intro N
  by_contra h
  push Not at h
  apply hα
  apply dyadic_of_eventually_zero (N := N)
  intro n hn
  rcases digit_zero_or_one α n with hz | ho
  · exact hz
  · exact False.elim (h n hn ho)

theorem not_dyadic_of_irrational {α : ℝ} (hα : Irrational α) : ¬ Dyadic α := by
  rintro ⟨n, z, rfl⟩
  exact hα ⟨(z : ℚ) / (2 : ℚ) ^ n, by norm_cast⟩

theorem irrational_unboundedOnes {α : ℝ} (hα : Irrational α) :
    UnboundedOnes (Ones α) :=
  unboundedOnes_of_not_dyadic (not_dyadic_of_irrational hα)

theorem height_tail_one {α : ℝ} {N : ℕ}
    (h : ∀ n, N ≤ n → digit α n = 1) (k : ℕ) :
    height α (N + k) = (2 : ℤ) ^ k * (height α N + 1) - 1 := by
  induction k with
  | zero => simp
  | succ k ih =>
    rw [Nat.add_succ, height_recurrence, h (N + k) (by omega), ih, pow_succ]
    ring

/-- The floor convention chooses the binary expansion with infinitely many zeros. -/
theorem unboundedZeros (α : ℝ) : UnboundedOnes (fun n => digit α n = 0) := by
  intro N
  by_contra hzero
  push Not at hzero
  have hone : ∀ n, N ≤ n → digit α n = 1 := by
    intro n hn
    rcases digit_zero_or_one α n with h | h
    · exact False.elim (hzero n hn h)
    · exact h
  let x : ℝ := (2 : ℝ) ^ N * α
  let z : ℤ := height α N
  have hx : x < (z : ℝ) + 1 := Int.lt_floor_add_one x
  have hpos : 0 < (z : ℝ) + 1 - x := by linarith
  obtain ⟨k, hkn⟩ := exists_nat_gt (1 / ((z : ℝ) + 1 - x))
  have hkpow : (k : ℝ) < (2 : ℝ) ^ k := by exact_mod_cast Nat.lt_two_pow_self
  have hk := (div_lt_iff₀ hpos).mp (lt_trans hkn hkpow)
  have hfloor := Int.floor_le ((2 : ℝ) ^ (N + k) * α)
  change (height α (N + k) : ℝ) ≤ _ at hfloor
  rw [height_tail_one hone k] at hfloor
  push_cast at hfloor
  dsimp [x, z] at hk
  rw [pow_add] at hfloor
  nlinarith

/-- Nondyadic parameters have arbitrarily late changes of adjacent digits. -/
theorem unboundedTransitions {α : ℝ} (hα : ¬ Dyadic α) :
    UnboundedOnes (fun n => digit α n ≠ digit α (n + 1)) := by
  intro N
  by_contra htrans
  push Not at htrans
  have hconstant : ∀ k : ℕ, digit α (N + k) = digit α N := by
    intro k
    induction k with
    | zero => simp
    | succ k ih =>
      rw [Nat.add_succ, ← htrans (N + k) (by omega), ih]
  obtain ⟨a, ha, hoa⟩ := unboundedOnes_of_not_dyadic hα N
  obtain ⟨b, hb, hzb⟩ := unboundedZeros α N
  have haeq := hconstant (a - N)
  have hbeq := hconstant (b - N)
  rw [Nat.add_sub_of_le ha] at haeq
  rw [Nat.add_sub_of_le hb] at hbeq
  dsimp [Ones] at hoa
  omega

end Erdos354Formal
end


/- Source: Completeness.lean -/
section
/- Indexed subset sums, interleaving, and the reduction to parameters at least one. -/

namespace Erdos354Formal

open Filter

def CompletePair (α β : ℝ) : Prop :=
  ∀ᶠ z : ℤ in atTop, ∃ s t : Finset ℕ,
    z = (∑ levelIndex ∈ s, height α levelIndex) + ∑ j ∈ t, height β j

theorem interleave_even (α β : ℝ) (n : ℕ) :
    Erdos354.FloorMultiples.interleave α β 2 (2 * n) = height α n := by
  simp [Erdos354.FloorMultiples.interleave, height]

theorem interleave_odd (α β : ℝ) (n : ℕ) :
    Erdos354.FloorMultiples.interleave α β 2 (2 * n + 1) = height β n := by
  simp [Erdos354.FloorMultiples.interleave, height, Nat.add_div]

theorem pair_sum_mem_subseqSums (α β : ℝ) (s t : Finset ℕ) :
    (∑ levelIndex ∈ s, height α levelIndex) + (∑ j ∈ t, height β j) ∈
      subseqSums' (Erdos354.FloorMultiples.interleave α β 2) := by
  classical
  let se := s.image (fun levelIndex => 2 * levelIndex)
  let oddIndices := t.image (fun levelIndex => 2 * levelIndex + 1)
  have hd : Disjoint se oddIndices := by
    apply Finset.disjoint_left.mpr
    intro z hz ht
    obtain ⟨levelIndex, _, hi⟩ := Finset.mem_image.mp hz
    obtain ⟨j, _, hj⟩ := Finset.mem_image.mp ht
    omega
  refine ⟨se ∪ oddIndices, ?_⟩
  rw [Finset.sum_union hd]
  dsimp [se, oddIndices]
  rw [Finset.sum_image (fun levelIndex _ j _ hij => by omega),
      Finset.sum_image (fun levelIndex _ j _ hij => by omega)]
  simp only [interleave_even, interleave_odd]

theorem CompletePair.isAddComplete {α β : ℝ} (h : CompletePair α β) :
    IsAddCompleteNatSeq' (Erdos354.FloorMultiples.interleave α β 2) := by
  filter_upwards [h] with z hz
  obtain ⟨s, t, rfl⟩ := hz
  exact pair_sum_mem_subseqSums α β s t

theorem subseqSums_comp_subset {A : ℕ → ℤ} {ι : ℕ → ℕ}
    (hι : Function.Injective ι) : subseqSums' (A ∘ ι) ⊆ subseqSums' A := by
  classical
  rintro z ⟨s, rfl⟩
  refine ⟨s.image ι, ?_⟩
  rw [Finset.sum_image (fun levelIndex _ j _ hij => hι hij)]
  rfl

theorem complete_of_complete_comp {A : ℕ → ℤ} {ι : ℕ → ℕ}
    (hι : Function.Injective ι) (h : IsAddCompleteNatSeq' (A ∘ ι)) :
    IsAddCompleteNatSeq' A := by
  filter_upwards [h] with z hz
  exact subseqSums_comp_subset hι hz

theorem height_scale (α : ℝ) (N n : ℕ) :
    height ((2 : ℝ) ^ N * α) n = height α (N + n) := by
  simp only [height, Erdos354.FloorMultiples, pow_add]
  congr 1
  ring

theorem interleave_scale (α β : ℝ) (N n : ℕ) :
    Erdos354.FloorMultiples.interleave ((2 : ℝ) ^ N * α) (2 ^ N * β) 2 n =
      Erdos354.FloorMultiples.interleave α β 2 (2 * N + n) := by
  have hm : (2 * N + n) % 2 = n % 2 := by omega
  have hd : (2 * N + n) / 2 = N + n / 2 := by omega
  simp only [Erdos354.FloorMultiples.interleave, hm, hd]
  split <;> exact height_scale _ _ _

theorem complete_of_dyadic_scale {α β : ℝ} (N : ℕ)
    (h : IsAddCompleteNatSeq'
      (Erdos354.FloorMultiples.interleave ((2 : ℝ) ^ N * α) (2 ^ N * β) 2)) :
    IsAddCompleteNatSeq' (Erdos354.FloorMultiples.interleave α β 2) := by
  apply complete_of_complete_comp (ι := fun n => 2 * N + n)
    (by intro levelIndex j h; dsimp at h; omega)
  simpa only [Function.comp_def, ← interleave_scale] using h

theorem exists_common_scale {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) :
    ∃ N : ℕ, 1 ≤ (2 : ℝ) ^ N * α ∧ 1 ≤ (2 : ℝ) ^ N * β := by
  obtain ⟨N, hN⟩ := exists_nat_gt (max (1 / α) (1 / β))
  have hpow : (N : ℝ) < (2 : ℝ) ^ N := by exact_mod_cast Nat.lt_two_pow_self
  have ha : 1 / α < (2 : ℝ) ^ N := lt_of_le_of_lt (le_max_left _ _) (hN.trans hpow)
  have hb : 1 / β < (2 : ℝ) ^ N := lt_of_le_of_lt (le_max_right _ _) (hN.trans hpow)
  exact ⟨N, ((div_lt_iff₀ hα).mp ha).le, ((div_lt_iff₀ hβ).mp hb).le⟩

/-- A proved reduction. The hypothesis is the remaining normalized completeness theorem. -/
theorem full_target_of_normalized
    (core : ∀ α β : ℝ, 1 ≤ α → 1 ≤ β → Irrational (α / β) → CompletePair α β) :
    True ↔ ∀ α > 0, ∀ β > 0, Irrational (α / β) →
      IsAddCompleteNatSeq' (Erdos354.FloorMultiples.interleave α β 2) := by
  constructor
  · intro _ α hα β hβ hirr
    obtain ⟨N, ha, hb⟩ := exists_common_scale hα hβ
    apply complete_of_dyadic_scale N
    apply CompletePair.isAddComplete
    apply core _ _ ha hb
    have hratio : ((2 : ℝ) ^ N * α) / (2 ^ N * β) = α / β := by
      field_simp
    simpa only [hratio] using hirr
  · intro _
    trivial

end Erdos354Formal
end


/- Source: Reduction.lean -/
section
/- The full arithmetic reduction to three explicitly stated dynamical criteria. -/

namespace Erdos354Formal

/-- If disjointness has the two digit criteria from the mathematical proof,
then every irrational-ratio pair of normalized parameters is disjoint. -/
theorem disjoint_of_digit_criteria (D : ℝ → ℝ → Prop)
    (hsymm : ∀ α β, D α β → D β α)
    (hbounded : ∀ α β, 1 ≤ α → 1 ≤ β → Irrational (α / β) →
      BoundedZeroRuns (Ones α) → D α β)
    (htransport : ∀ α β, 1 ≤ α → 1 ≤ β → Irrational (α / β) →
      UnboundedOnes (Ones α) → ¬ D α β →
      ∃ b, 0 < b ∧ ForwardTransport (Ones α) (Ones β) b)
    (α β : ℝ) (hα : 1 ≤ α) (hβ : 1 ≤ β) (hirr : Irrational (α / β)) :
    D α β := by
  have key : ∀ α β : ℝ, 1 ≤ α → 1 ≤ β → Irrational (α / β) →
      UnboundedOnes (Ones α) → D α β := by
    intro a b ha hb hir hones
    by_contra hnot
    obtain ⟨s, hs, hAB⟩ := htransport a b ha hb hir hones hnot
    have hB := hAB.unbounded hones
    have hir' : Irrational (b / a) := by simpa only [inv_div] using hir.inv
    have hnot' : ¬ D b a := fun h => hnot (hsymm b a h)
    obtain ⟨t, ht, hBA⟩ := htransport b a hb ha hir' hB hnot'
    exact hnot (hbounded a b ha hb hir
      (boundedZeroRuns_of_two_transports hs ht hones hAB hBA))
  rcases hirr.div_cases with ha | hb
  · exact key α β hα hβ hirr (irrational_unboundedOnes ha)
  · have hirr' : Irrational (β / α) := by simpa only [inv_div] using hirr.inv
    exact hsymm β α (key β α hβ hα hirr' (irrational_unboundedOnes hb))

/-- The remaining assumptions are the joining obstruction, the bounded-zero
criterion, and the carry-to-transport criterion. This is a conditional reduction,
not a proof of `Bounty.target`. -/
theorem full_target_of_dynamical_criteria (D : ℝ → ℝ → Prop)
    (hsymm : ∀ α β, D α β → D β α)
    (hjoining : ∀ α β, 1 ≤ α → 1 ≤ β → D α β → CompletePair α β)
    (hbounded : ∀ α β, 1 ≤ α → 1 ≤ β → Irrational (α / β) →
      BoundedZeroRuns (Ones α) → D α β)
    (htransport : ∀ α β, 1 ≤ α → 1 ≤ β → Irrational (α / β) →
      UnboundedOnes (Ones α) → ¬ D α β →
      ∃ b, 0 < b ∧ ForwardTransport (Ones α) (Ones β) b) :
    True ↔ ∀ α > 0, ∀ β > 0, Irrational (α / β) →
      IsAddCompleteNatSeq' (Erdos354.FloorMultiples.interleave α β 2) := by
  apply full_target_of_normalized
  intro α β hα hβ hirr
  exact hjoining α β hα hβ
    (disjoint_of_digit_criteria D hsymm hbounded htransport α β hα hβ hirr)

end Erdos354Formal
end


/- Source: FiniteSums.lean -/
section
/- Finite binary subset-sum recursion, support bounds, and exact cardinality. -/

namespace Erdos354Formal

def finiteSums (a : ℕ → ℤ) : ℕ → Finset ℤ
  | 0 => {0}
  | n + 1 => finiteSums a n ∪ (finiteSums a n).image (fun z => z + a n)

theorem mem_finiteSums_iff (a : ℕ → ℤ) (n : ℕ) (z : ℤ) :
    z ∈ finiteSums a n ↔ ∃ s : Finset ℕ, s ⊆ Finset.range n ∧ z = ∑ levelIndex ∈ s, a levelIndex := by
  classical
  induction n generalizing z with
  | zero => simp [finiteSums]
  | succ n ih =>
    constructor
    · intro hz
      rcases Finset.mem_union.mp hz with hz | hz
      · obtain ⟨s, hs, hsum⟩ := (ih z).mp hz
        exact ⟨s, hs.trans (Finset.range_mono (by omega)), hsum⟩
      · obtain ⟨y, hy, rfl⟩ := Finset.mem_image.mp hz
        obtain ⟨s, hs, rfl⟩ := (ih y).mp hy
        have hn : n ∉ s := by
          intro h
          have := Finset.mem_range.mp (hs h)
          omega
        refine ⟨insert n s, ?_, ?_⟩
        · rw [Finset.range_add_one]
          exact Finset.insert_subset_insert n hs
        · rw [Finset.sum_insert hn]
          ring
    · rintro ⟨s, hs, rfl⟩
      by_cases hn : n ∈ s
      · have he : s.erase n ⊆ Finset.range n := by
          intro levelIndex hi
          obtain ⟨hin, his⟩ := Finset.mem_erase.mp hi
          have hir := Finset.mem_range.mp (hs his)
          exact Finset.mem_range.mpr (by omega)
        apply Finset.mem_union_right
        apply Finset.mem_image.mpr
        refine ⟨∑ levelIndex ∈ s.erase n, a levelIndex, (ih _).mpr ⟨s.erase n, he, rfl⟩, ?_⟩
        exact Finset.sum_erase_add _ _ hn
      · apply Finset.mem_union_left
        apply (ih _).mpr
        refine ⟨s, ?_, rfl⟩
        intro levelIndex hi
        have hir := Finset.mem_range.mp (hs hi)
        have hin : levelIndex ≠ n := by rintro rfl; exact hn hi
        exact Finset.mem_range.mpr (by omega)

theorem mem_subseqSums_iff_exists_finiteSums (a : ℕ → ℤ) (z : ℤ) :
    z ∈ subseqSums' a ↔ ∃ n, z ∈ finiteSums a n := by
  constructor
  · rintro ⟨s, hsum⟩
    obtain ⟨n, hn⟩ := Finset.exists_nat_subset_range s
    exact ⟨n, (mem_finiteSums_iff a n z).mpr ⟨s, hn, hsum⟩⟩
  · rintro ⟨n, hn⟩
    obtain ⟨s, _, hsum⟩ := (mem_finiteSums_iff a n z).mp hn
    exact ⟨s, hsum⟩

theorem finiteSums_bounds {α : ℝ} (hα : 1 ≤ α) (n : ℕ) {z : ℤ}
    (hz : z ∈ finiteSums (height α) n) : 0 ≤ z ∧ z < height α n := by
  obtain ⟨s, hs, rfl⟩ := (mem_finiteSums_iff _ _ _).mp hz
  constructor
  · exact Finset.sum_nonneg fun levelIndex _ => (height_positive hα levelIndex).le
  · apply lt_of_le_of_lt _ (sum_height_lt hα n)
    exact Finset.sum_le_sum_of_subset_of_nonneg hs
      (fun levelIndex _ _ => (height_positive hα levelIndex).le)

theorem finiteSums_disjoint_shift {α : ℝ} (hα : 1 ≤ α) (n : ℕ) :
    Disjoint (finiteSums (height α) n)
      ((finiteSums (height α) n).image (fun z => z + height α n)) := by
  apply Finset.disjoint_left.mpr
  intro z hz hshift
  obtain ⟨y, hy, rfl⟩ := Finset.mem_image.mp hshift
  have h₁ := finiteSums_bounds hα n hz
  have h₂ := finiteSums_bounds hα n hy
  omega