Regular geometry at all stable excursion levels

Compact interior bounds come from the sealed rational-window minimum theorem. Rational non-jump levels supply record brackets on both sides; right brackets use right continuity of the strict passage process.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.ae_isRegularExcursionLevel {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, IsRegularExcursionLevel f x

A.s. supplier of the geometric facts (iii): every jump level is a regular excursion level (interior bounds for values AND left limits, strict record brackets, zero endpoints).