Finite cylinders of consecutive ladder blocks

Concatenated degree words locate each ladder boundary without using a random restart. Conversely the first finitely many ladder blocks concatenate to the corresponding initial offspring word.

theorem BGW.StableTrees.DiscreteForest.seqPrefix_add (m n : ℕ) (ω : ℕ → ℕ) : seqPrefix (m + n) ω = seqPrefix m ω ++ seqPrefix n (shiftSeq m ω)

Splitting an offspring prefix at a deterministic time concatenates degree words.

theorem BGW.StableTrees.DiscreteForest.ladderTime_of_forest_prefix (ω : ℕ → ℕ) (ts : PlaneForest) (hpre : seqPrefix ts.size ω = ts.degrees) : ladderTime ω (List.length ts) = ts.size

A finite forest word ends at the first hitting of minus its number of roots.

noncomputable def BGW.StableTrees.DiscreteForest.blockPrefix (r : ℕ) (ω : ℕ → ℕ) : PlaneForest

The first r decoded trees in component order.

Equations

• BGW.StableTrees.DiscreteForest.blockPrefix r ω = List.ofFn fun (i : Fin r) => BGW.StableTrees.DiscreteForest.blockTree ω ↑i

theorem BGW.StableTrees.DiscreteForest.degrees_blockPrefix {ω : ℕ → ℕ} (hω : LadderFinite ω) (r : ℕ) : (blockPrefix r ω).degrees = seqPrefix (ladderTime ω r) ω

The first finitely many blocks concatenate to the initial offspring word.

theorem BGW.StableTrees.DiscreteForest.blockPrefix_eq_iff {ω : ℕ → ℕ} (hω : LadderFinite ω) (ts : PlaneForest) : blockPrefix (List.length ts) ω = ts ↔ seqPrefix ts.size ω = ts.degrees

A forest degree-word cylinder is exactly a cylinder of initial ladder trees.

theorem BGW.StableTrees.DiscreteForest.blockPrefix_mass (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (ts : PlaneForest) : ↑(offspringSeqLaw μ) {ω : ℕ → ℕ | blockPrefix (List.length ts) ω = ts} = (List.map (PlaneTree.weight ⇑μ) ts).prod

The mass of a cylinder prescribing the first finitely many tree blocks.