Exponential form of the ladder Laplace semigroup

The rational-level argument for a positive monotone multiplicative function follows the existing no-arrival Cauchy proof, with strict positivity supplied by the integral itself.

theorem BGW.StableTrees.exists_supLadderLaplace_eq_exp {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 ≤ q) (hlam : 0 ≤ lam) : ∃ (k : ℝ), 0 ≤ k ∧ ∀ (z : NNReal), supLadderLaplace θ q lam z = Real.exp (-↑z * k)

Exponential form (measurable multiplicative Cauchy equation, positivity from φ(z/2ⁿ) → 1): there is a rate k ≥ 0 with φ(z) = e^{-zk} for all z.