Scale-uniform cycle second moments

The renewal estimate controls the quadratic term. The remaining linear ceiling term vanishes at every fixed positive band parameter.

theorem BGW.StableTrees.DiscreteHeightApprox.limsup_clusterVisits_sq_le {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {ε : ℝ} (hε : 0 < ε) : Filter.limsup (fun (n : ℕ) => ENNReal.ofReal ((B n / ↑n * ∫ (ω : ℕ → ℕ), ↑(clusterVisits ω (ε * B n) 0) ^ 2 ∂↑(DiscreteForest.offspringSeqLaw μ)) / (ε * B n) ^ 2)) Filter.atTop ≤ ENNReal.ofReal (17 * Real.exp 1 * ε ^ (θ - 1))

A fixed positive band has normalized cycle second-moment limsup of order ε^(θ-1), with a universal numerical constant.

theorem BGW.StableTrees.DiscreteHeightApprox.clusterVisits_secondMoment_scaled {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) : Filter.Tendsto (fun (ε : ℝ) => Filter.limsup (fun (n : ℕ) => ENNReal.ofReal ((B n / ↑n * ∫ (ω : ℕ → ℕ), ↑(clusterVisits ω (ε * B n) 0) ^ 2 ∂↑(DiscreteForest.offspringSeqLaw μ)) / (ε * B n) ^ 2)) Filter.atTop) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Scale-free second moment of a cycle at level a = ε B_n against N ≈ n/B_n cycles: limsup_{ε↓0} limsup_n (B_n/n) E[V_0(εB_n)²] / (ε B_n)² = 0 (rate ε^{θ-1} by the renewal bound).