Fringe subtrees as contiguous DFS blocks

At the vertex in DFS position i, the fringe subtree occupies a contiguous block of the increment word beginning at i. Rotating to this position and stopping at the first passage to -1 therefore recovers exactly that fringe subtree.

This is eq:fringe in Section 2.1 of Kortchemski–Vetter, Rare subtree patterns in size-conditioned Bienaymé trees (source lines 691–696). The block induction adapts PoissonDeclumping/Lukasiewicz/Coding.lean, dfsSeq_fringeTrees_prefix. Here the fringe is identified by its actual address, and the decoder accepts an entire finite word; the bounded prefix characterization does not claim that it accepts an untruncated rotation.

theorem BGW.PlaneTree.increments_fringe_prefix {t s : PlaneTree} {u : List ℕ} {i : ℕ} (hi : t.vertices[i]? = some u) (hs : t.fringe? u = some s) : s.increments <+: List.drop i t.increments

The fringe at DFS index i occupies a contiguous block beginning at that index.

theorem BGW.PlaneTree.take_rotate_increments_fringe {t s : PlaneTree} {u : List ℕ} {i : ℕ} (hi : t.vertices[i]? = some u) (hs : t.fringe? u = some s) : List.take s.size (t.increments.rotate i) = s.increments

Rotating to a vertex and taking its fringe size gives exactly the fringe code. Its total sum is -1, and every shorter prefix sum is nonnegative.

theorem BGW.PlaneTree.ofIncrements?_take_rotate_eq_some_iff {t s : PlaneTree} {u : List ℕ} {i m : ℕ} (hi : t.vertices[i]? = some u) (hm : m ≤ t.size) : ofIncrements? (List.take m (t.increments.rotate i)) = some s ↔ t.fringe? u = some s ∧ m = s.size

The only accepted bounded prefix of a rotation is the complete fringe code at that vertex. The bound on m prevents the saturation of List.take from giving longer apparent cut times.