Exclusion of long plateaus before the selected excursion

A constant running infimum on a nontrivial interval belongs to a passage jump. The lifetime threshold and the least-long-label property exclude such intervals of length at least one before the first long excursion.

theorem BGW.StableTrees.GoodLongExtractionPath.isLeast_firstLongLabel {M : NNReal} {f : Skorokhod.DLoc} (hf : GoodLongExtractionPath M f) : IsLeast (longLabelSet f) (firstLongLabel f)

The selected label is the least long label under the good-path predicate. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.no_long_runningInf_plateau_ending_early {M : NNReal} {f : Skorokhod.DLoc} (hf : GoodLongExtractionPath M f) {a b : NNReal} (hlen : 1 ≤ b - a) (hb : b < passageTimeMinus (firstLongLabel f) f + 1) : runningInfLoc f a ≠ runningInfLoc f b

No unit-long plateau can end before one unit after the selected start. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.no_long_runningInf_plateau_before_firstLong {M : NNReal} {f : Skorokhod.DLoc} (hf : GoodLongExtractionPath M f) {a b : NNReal} (hlen : 1 ≤ b - a) (hb : b ≤ passageTimeMinus (firstLongLabel f) f) : runningInfLoc f a ≠ runningInfLoc f b

No interval of length at least one before the selected start has constant running infimum. Reference: Billingsley (1999), Chapter 3.