Nonsummable progression weights force record-charge divergence

import Definitions.Def_ErdosProblems_Erdos243_ReciprocalTailRigidity
import Definitions.Def_ErdosProblems_Erdos243_LcmRecordCrossing
import Definitions.Def_ErdosProblems_Erdos243_LcmRecordDivergence
import Mathlib
import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
import Mathlib.Analysis.SpecificLimits.Basic
import Mathlib.Data.Fin.Pigeonhole
import Mathlib.Data.Nat.ChineseRemainder
import Mathlib.Data.Nat.Find
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.ZMod.Basic
import Mathlib.Order.Filter.AtTopBot.Basic
import Mathlib.Tactic.Ring

/-!
# From finite first crossings to divergent record mass

This module transfers nonsummability of the actual progression weights to
the record-excess series. The sequence need only reach arbitrarily large
heights; no monotonicity or limit at infinity is assumed. The analytic input
that a particular weight has divergent progression sum remains explicit.
-/

open ErdosProblems.Erdos243.LcmRecordCrossing

theorem ErdosProblems.Erdos243.LcmRecordCrossing.not_summable_recordExcessWeight_of_progression
    (U : ℕ → ℕ) (a L : ℕ → ℤ) (x P B : ℕ) (hP : B < P)
    (hzero : U 0 < x)
    (hunbounded : ∀ t : ℕ, ∃ n, t ≤ U n)
    (hfeedback : ∀ n, (∀ j ≤ n, U j < U (n + 1)) →
      ((U (n + 1) - U n : ℕ) : ℤ) = (a n - 1) * U n - L n)
    (hcover : ∀ n k : ℕ, ∀ z : ℤ,
      (x + k * P : ℕ) - (B : ℤ) ≤ z → z < (x + k * P : ℕ) →
      ∃ m : ℤ, (B : ℤ) < m ∧ m ∣ L n ∧ m ∣ z)
    (f : ℕ → ℝ) (hf : Antitone f) (hpos : ∀ u, 0 ≤ f u)
    (hdiverges : ¬ Summable (fun k : ℕ => f (x + k * P))) :
    ¬ Summable (recordExcessWeight U B f) := by sorry