Crude depth guard, natural-number form

Let $E, s, m, d, C_1 \in \mathbb N$ with $s, m \ge 2$, $d \ge 1$, $2 + m \log s \le C_1$, and $0 \le \beta \le 1$. If $A : \mathbb N \to \mathbb N$ satisfies the crude-guard recursion (at most $s$ children $c$ with $mc \le (m-1)e$ and $A(e) \le E + \sum_c A(c)$ for $e \ge d^{\beta}$, and $A(e) \le 8 d^{\beta}$ for $e < d^{\beta}$), then for all $e \le d$

In Lean:

theorem R6.crude_guard_nat (E s m d C1 : ℕ) (β : ℝ) (A : ℕ → ℕ) (hm : 2 ≤ m) (hs : 2 ≤ s)
    (hβ : 0 ≤ β ∧ β ≤ 1) (hd : 1 ≤ d) (hC1 : 2 + m * Real.log s ≤ C1)
    (hrec : ∀ e : ℕ, (d : ℝ) ^ β ≤ e → ∃ cs : List ℕ, cs.length ≤ s ∧
      (∀ c ∈ cs, m * c ≤ (m - 1) * e) ∧ A e ≤ E + (cs.map A).sum)
    (hleaf : ∀ e : ℕ, (e : ℝ) < (d : ℝ) ^ β → (A e : ℝ) ≤ 8 * (d : ℝ) ^ β) :
    ∀ e : ℕ, e ≤ d → A e ≤ 2 * s * (E + 8) * d ^ C1

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*).