The binary case of Marchal growth

At α = 2, internal positions of a binary tree have weight zero and edge positions have weight one. Edge grafts therefore give Rémy growth.

theorem BGW.StableTrees.Marchal.selectionWeight_two_binary {n : ℕ} (T : LTree n) (hb : ∀ (v : Fin T.m), T.G.degree v = 1 ∨ T.G.degree v = 3) (p : ↑T.G.edgeSet ⊕ { v : Fin T.m // 3 ≤ T.G.degree v }) : selectionWeight T.G 2 p = match p with | Sum.inl val => 1 | Sum.inr val => 0

At α = 2, on a binary tree every internal vertex has weight zero (d - 1 - α = 0): only edges are selected.

theorem BGW.StableTrees.Marchal.graft_inl_binary {n : ℕ} (T : LTree n) (e : ↑T.G.edgeSet) (hb : ∀ (v : Fin T.m), T.G.degree v = 1 ∨ T.G.degree v = 3) (y : Fin (T.m + 2)) : (graftGraph T.G (Sum.inl e)).degree y = 1 ∨ (graftGraph T.G (Sum.inl e)).degree y = 3

Edge grafting preserves binary trees.

theorem BGW.StableTrees.Marchal.startState_binary : startState.IsBinary

The initial edge is binary.

theorem BGW.StableTrees.Marchal.lawWeight_two_binary {n : ℕ} (T : LTree n) (hb : ∀ (v : Fin T.m), T.G.degree v = 1 ∨ T.G.degree v = 3) : LTree.lawWeight 2 T = 1

At α = 2, the numerator is one on every binary tree.

theorem BGW.StableTrees.Marchal.prod_two_denominator (k : ℕ) : ∏ j ∈ Finset.range k, (↑(j + 1) * 2 - 1) = ↑(2 * (k + 1) - 3).doubleFactorial

The odd-factor denominator is the corresponding double factorial.

theorem BGW.StableTrees.Marchal.law_two_support_binary (k : ℕ) : (law law_two_support_binary._proof_1 ⋯ k).support ⊆ {s : State (k + 1) | s.IsBinary}

α = 2 support: only binary states have positive mass (all steps from A_0 — A_1).

theorem BGW.StableTrees.Marchal.step_two_binary (k : ℕ) (T : LTree (k + 1)) (hb : ∀ (v : Fin T.m), T.G.degree v = 1 ∨ T.G.degree v = 3) (t : State (k + 2)) : (step law_two_support_binary._proof_1 ⋯ k ⟦T⟧) t = ↑{e : ↑T.G.edgeSet | ⟦graft T (Sum.inl e)⟧ = t}.ncard / ↑(2 * k + 1)

α = 2 step is Rémy's step: from a binary state, graft at a uniformly chosen one of the 2k+1 edges (no plane order is involved: states are non-plane).