The integer and real ladder-block coding adapter

Finite ladder times identify K02's equality hits and K04's weak real hits, their selected indices, and the closed increments of the decoded first long tree.

def BGW.StableTrees.PathTail.realForestIncrements (ω : ℕ → ℕ) (i : ℕ) : ℝ

Real offspring-minus-one increments, matching the sealed forest pushforward.

Equations

• BGW.StableTrees.PathTail.realForestIncrements ω i = ↑↑(ω i) - 1

theorem BGW.StableTrees.PathTail.hitTime_eq {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (r : ℕ) : walkHitTime r (realForestIncrements ω) = ↑(DiscreteForest.ladderTime ω r)

The real walk's hitting time is the discrete ladder time on a finite ladder.

theorem BGW.StableTrees.PathTail.ladderTime_eq {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (r : ℕ) : ladderTime (realForestIncrements ω) r = DiscreteForest.ladderTime ω r

Real and discrete ladder times agree on a finite ladder.

theorem BGW.StableTrees.PathTail.firstLongIndex_eq {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (n : ℕ) : firstLongIndex n (realForestIncrements ω) = DiscreteForest.firstLongIndex n ω

Real and discrete first-long-block indices agree on a finite ladder.

theorem BGW.StableTrees.PathTail.closedTreeIncrementSeq_firstLongTree {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (n : ℕ) : closedTreeIncrementSeq (DiscreteForest.firstLongTree n ω) = blockIncrements (realForestIncrements ω) (firstLongIndex n (realForestIncrements ω))

K02 first-long-tree closed increments agree exactly with K04 selected block increments.