Restart and independence of weak ascending cycles

History events are saturated under agreement up to the genuine extended epoch. They are pre-stopped events on every sequence, while agreeing almost surely with the finite-cycle history. This keeps totalized epochs out of the stopping-time premise.

theorem BGW.StableTrees.DiscreteHeightApprox.clusterVisits_history_factor (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (a : ℝ) (i : ℕ) (S : Finset ℕ) (hS : ∀ j ∈ S, j < i) (A : ℕ → Set ℕ) {C : Set ℕ} (hC : MeasurableSet C) : ↑(DiscreteForest.offspringSeqLaw μ) ({ω : ℕ → ℕ | ∀ j ∈ S, clusterVisits ω a j ∈ A j} ∩ {ω : ℕ → ℕ | clusterVisits ω a i ∈ C}) = ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | ∀ j ∈ S, clusterVisits ω a j ∈ A j} * ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | clusterVisits ω a 0 ∈ C}

Restart at the next cycle factors its occupation from every preceding finite cycle history.

theorem BGW.StableTrees.DiscreteHeightApprox.map_clusterVisits_eq_zero (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (a : ℝ) (i : ℕ) : MeasureTheory.Measure.map (fun (ω : ℕ → ℕ) => clusterVisits ω a i) ↑(DiscreteForest.offspringSeqLaw μ) = MeasureTheory.Measure.map (fun (ω : ℕ → ℕ) => clusterVisits ω a 0) ↑(DiscreteForest.offspringSeqLaw μ)

Every weak-cycle occupation has the first cycle's distribution.

theorem BGW.StableTrees.DiscreteHeightApprox.clusterVisits_iid (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {a : ℝ} (ha : 0 < a) : ProbabilityTheory.iIndepFun (fun (i : ℕ) (ω : ℕ → ℕ) => clusterVisits ω a i) ↑(DiscreteForest.offspringSeqLaw μ) ∧ ∀ (i : ℕ), MeasureTheory.Measure.map (fun (ω : ℕ → ℕ) => clusterVisits ω a i) ↑(DiscreteForest.offspringSeqLaw μ) = MeasureTheory.Measure.map (fun (ω : ℕ → ℕ) => clusterVisits ω a 0) ↑(DiscreteForest.offspringSeqLaw μ)

(Stopped restart at the epochs) the cycle visit counts are iid under the offspring law.