Exponential erased-height tail

The ancestral source bounds erasure by a passage-stopped reversed clock. Rational clock barriers transfer with an independent fresh depth to the stable product law, where the full ladder transform bounds them. The constant extension of the reversal is never given the full stable law, and continuity of the height process is not used.

theorem BGW.StableTrees.erased_height_tail_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t r : NNReal) (hr : 0 < r) (v : ℝ) (hv : 0 ≤ v) : ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | v < height θ f t - ↑(topHeight (eraseMass (ENNReal.ofReal (-futureInf (Skorokhod.DLoc.shift t f) r 0)) (exploration θ f t)))} ≤ ENNReal.ofReal (Real.exp 1 * Real.exp (-(v * ↑r ^ (-(1 - 1 / θ)))))

Erased-height tail. PROOF REQUIREMENT: use an independent fresh depth and a stopped/full ladder bound, without height continuity; reversal is constant after t, so its unrestricted ladder height is not an independent full stable process.