Height bridges from exploration erasure

The common reversed clock identifies the surviving support top and the fresh height. Erasure preserves every upper support bound, including complete erasure. The approximation has measurable limits under the excursion and unit laws. Predicate diagonalization supplies one sequence for the stable, excursion and unit laws, both at rational ages and at almost every age. The universal height is the literal limsup along that sequence. The erased-height tail uses the ancestral source, a passage-stopped reversed clock, independence of the fresh depth, and the full stable ladder transform. No continuation of the reversed path is constructed.

theorem BGW.StableTrees.topHeight_eraseMass_le {ρ : MeasureTheory.Measure NNReal} {R : NNReal} (hρ : ρ (Set.Ioi R) = 0) (m : ENNReal) : topHeight (eraseMass m ρ) ≤ R

A mass-free upper tail bounds the support top after erasure.

theorem BGW.StableTrees.ae_height_erasure_decomposition {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t r : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), have m := ENNReal.ofReal (-futureInf (Skorokhod.DLoc.shift t f) r 0); have K := ↑(topHeight (eraseMass m (exploration θ f t))); 0 ≤ K ∧ K ≤ height θ f t ∧ height θ f (t + r) = K + height θ (Skorokhod.DLoc.shift t f) r

Erasure decomposition (fixed t, r): with m the mass erased by the future infimum and K the height of what survives erasure, a.s. 0 ≤ K ≤ H_t and H_{t+r} = K + H'_r.