First passage at forest component boundaries

An ordered forest is encoded by concatenating its component increment sequences. Its path first reaches minus the number of components at its terminal time. More generally, the end of the first r components is the first visit to -r. The statements use finite prefix sums and include the empty forest.

@[simp]

theorem BGW.PlaneForest.increments_append (ts ss : PlaneForest) : (ts ++ ss).increments = ts.increments ++ ss.increments

theorem BGW.PlaneForest.sum_take_increments_gt (ts : PlaneForest) {i : ℕ} (hi : i < ts.increments.length) : -↑(List.length ts) < (List.take i ts.increments).sum

A forest path stays strictly above its terminal level before its final step.

theorem BGW.PlaneForest.take_increments_size_take (ts : PlaneForest) (r : ℕ) : List.take (size (List.take r ts)) ts.increments = increments (List.take r ts)

The first r components occupy exactly their total size in the full code. This also holds when r exceeds the component count, since List.take saturates.

theorem BGW.PlaneForest.sum_take_increments_size_take (ts : PlaneForest) {r : ℕ} (hr : r ≤ List.length ts) : (List.take (size (List.take r ts)) ts.increments).sum = -↑r

At the end of the first r components, the path has value -r.

theorem BGW.PlaneForest.sum_take_increments_gt_before_size_take (ts : PlaneForest) {r i : ℕ} (hr : r ≤ List.length ts) (hi : i < size (List.take r ts)) : -↑r < (List.take i ts.increments).sum

The path has not yet reached -r before the end of the first r components.