Exploration restart from a common reversed clock

Capping the old source erases its top mass under the monotone ancestral height clock. The fresh reversal agrees with the initial common reversed window, so ancestral clock additivity translates fresh heights by the clock offset. Old and fresh source heights lie on opposite sides of that offset. Fixed-time gap-freeness identifies it with the surviving old support top, without evaluating height at a separately chosen crossing time.

The contact additivity used here is inherited from height_ancestor_clock_identity. The fresh path law is the sealed deterministic-time Markov law. All source almost-everywhere statements use Stieltjes ancestral concentration, with the old endpoint retained.

theorem BGW.StableTrees.ae_exploration_old_source {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t r : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), MeasureTheory.Measure.map (fun (x : ℝ) => (height θ f x.toNNReal).toNNReal) ((explorationStieltjes f (t + r)).measure.restrict (Set.Ioc 0 ↑t)) = eraseMass (ENNReal.ofReal (-futureInf (Skorokhod.DLoc.shift t f) r 0)) (exploration θ f t)

The source before a fixed restart pushes forward to the erased old exploration.

theorem BGW.StableTrees.reversedAt_shift_prefix (f : Skorokhod.DLoc) (t r : NNReal) (ht : Function.leftLim (↑f) t = ↑f t) {u : NNReal} (hu : u ≤ r) : ↑(reversedAt r (Skorokhod.DLoc.shift t f)) u = ↑(reversedAt (t + r) f) u

Reversing a shifted path gives the same initial reversed window at a continuity point.

theorem BGW.StableTrees.supLocalTime_reversedAt_shift_prefix (θ : ℝ) (f : Skorokhod.DLoc) (t r : NNReal) (ht : Function.leftLim (↑f) t = ↑f t) {u : NNReal} (hu : u ≤ r) : supLocalTime θ (reversedAt r (Skorokhod.DLoc.shift t f)) u = supLocalTime θ (reversedAt (t + r) f) u

The clocks on a fresh reversed window agree with the common reversed clock.

theorem BGW.StableTrees.ae_exploration_source_clock {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {T : NNReal} (hT : 0 < T) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ᵐ (x : ℝ) ∂(explorationStieltjes f T).measure.restrict (Set.Ioc 0 ↑T), 0 < x ∧ x ≤ ↑T ∧ 0 ≤ height θ f x.toNNReal ∧ height θ f x.toNNReal = supLocalTime θ (reversedAt T f) T - supLocalTime θ (reversedAt T f) (T - x.toNNReal)

At a fixed horizon, the source height is the terminal clock minus its reversed-age clock.

theorem BGW.StableTrees.exploration_source_order_bounds (θ : ℝ) (f : Skorokhod.DLoc) (t r : NNReal) (hmono : Monotone fun (u : ↑(Set.Iic (t + r))) => supLocalTime θ (reversedAt (t + r) f) ↑u) (hclock : ∀ᵐ (x : ℝ) ∂(explorationStieltjes f (t + r)).measure.restrict (Set.Ioc 0 ↑(t + r)), 0 < x ∧ x ≤ ↑(t + r) ∧ 0 ≤ height θ f x.toNNReal ∧ height θ f x.toNNReal = supLocalTime θ (reversedAt (t + r) f) (t + r) - supLocalTime θ (reversedAt (t + r) f) (t + r - x.toNNReal)) : have K := supLocalTime θ (reversedAt (t + r) f) (t + r) - supLocalTime θ (reversedAt (t + r) f) r; (MeasureTheory.Measure.map (fun (x : ℝ) => (height θ f x.toNNReal).toNNReal) ((explorationStieltjes f (t + r)).measure.restrict (Set.Ioc 0 ↑t))) (Set.Ioi K.toNNReal) = 0 ∧ (MeasureTheory.Measure.map (fun (x : ℝ) => (height θ f x.toNNReal).toNNReal) ((explorationStieltjes f (t + r)).measure.restrict (Set.Ioc ↑t ↑(t + r)))) (Set.Iio K.toNNReal) = 0

The common reversed clock orders the old and fresh source heights around its offset.

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

The surviving old exploration has support top equal to the common-clock offset.

theorem BGW.StableTrees.ae_exploration_fresh_height_translation {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t r : NNReal) (hr : 0 < r) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ᵐ (x : ℝ) ∂(explorationStieltjes (Skorokhod.DLoc.shift t f) r).measure.restrict (Set.Ioc 0 ↑r), (height θ f (↑t + x).toNNReal).toNNReal = (height θ (Skorokhod.DLoc.shift t f) x.toNNReal).toNNReal + topHeight (eraseMass (ENNReal.ofReal (-futureInf (Skorokhod.DLoc.shift t f) r 0)) (exploration θ f t))

Fresh source heights add the support top of the surviving old exploration.

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

Restart identity (a.s., for fixed t and r): with f' = shift t f the centered future, ρ_{t+r}(f) is ρ_t(f) with the top -inf_{[0,r]} f' units of mass erased and the fresh exploration ρ_r(f') appended above the remaining support height.