Generic crude depth guard for recursions with shrinking children

Let $A : \mathbb N \to \mathbb R$, $E, L \ge 0$, $T > 0$, $s, m \ge 2$. Suppose that every $e \ge T$ has a list of at most $s$ children $c$ with $m c \le (m-1) e$ and $A(e) \le E + \sum_c A(c)$, and that $A(e) \le L$ for $e < T$. Then for every $e$

This is the crude bound on the size of a recursion tree whose children shrink by the factor $(m-1)/m$; it is the common core of the depth-guard estimates below.

In Lean:

theorem R6.guard_gen (E L T : ℝ) (s m : ℕ) (A : ℕ → ℝ) (hm : 2 ≤ m) (hs : 2 ≤ s) (hE : 0 ≤ E)
    (hL : 0 ≤ L) (hT : 0 < T)
    (hrec : ∀ e : ℕ, T ≤ e → ∃ cs : List ℕ, cs.length ≤ s ∧ (∀ c ∈ cs, m * c ≤ (m - 1) * e) ∧
      A e ≤ E + (cs.map A).sum)
    (hleaf : ∀ e : ℕ, (e : ℝ) < T → A e ≤ L) :
    ∀ e : ℕ, A e ≤ (E + L) * (2 * (s : ℝ) ^ (max 0 (m * (Real.log e - Real.log T) + 1)) - 1)

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).