Spectral positivity of the stable process

The offspring-law witness of exists_stableDomain has no step below -1. Its reciprocal-normalizer jump bound passes to the unique limiting law by the closed-set inequality in the Portmanteau theorem (Billingsley, Convergence of Probability Measures, 2nd ed., 1999, Theorem 2.1). The limit is spectrally positive; Bertoin, Lévy Processes, 1996, Chapter VII, treats the mirror image (spectrally negative processes).

theorem BGW.StableTrees.ae_leftLim_le_stableProcessLaw {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑(stableProcessLaw θ T), ∀ (t : ↑(Set.Icc 0 T)), Function.leftLim (⇑f) t ≤ f t

Almost surely, simultaneously at all times t ∈ [0,T], the path has no negative jump: f (t-) ≤ f t. Proved through the offspring witness (steps ≥ -1) and uniqueness, not through the absence of fixed discontinuities.