The Graded Cut Identity and the Flow Identity

This file proves the combinatorial identity underlying the flow property of the exact B-series: for every ordered forest, the sum of inverse tree factorials over the coproduct terms whose trunk has k vertices is a binomial multiple of the inverse forest factorial,

Σ_{cuts, |R^c| = k} 1/(P^c! R^c!) = C(|ω|, k) / ω!,

and consequently the two-variable flow identity

Σ_{cuts} h^{|P^c|}/P^c! · h'^{|R^c|}/R^c! = (h + h')^{|ω|} / ω!,

which expresses that the exact flows compose: B_h ∘ B_{h'} = B_{h+h'} (Butcher; Hairer-Lubich-Wanner, Geometric Numerical Integration, III.1). The tree case reduces along the B⁺ recursion of the coproduct via Nat.add_one_mul_choose_eq, and the forest case is Vandermonde's identity.

noncomputable def BSeries.PTree.gradedCutSumList (R : Type u) [Field R] (ts : List HopfAlgebras.PTree) (k : ℕ) : R

The k-graded sum of inverse tree factorials over the coproduct terms of an ordered forest: cut terms whose trunk has k vertices.

Equations

• One or more equations did not get rendered due to their size.

theorem BSeries.PTree.gradedCutSumList_eq (R : Type u) [Field R] [CharZero R] (ts : List HopfAlgebras.PTree) (k : ℕ) : gradedCutSumList R ts k = ↑((HopfAlgebras.PTree.orderList ts).choose k) * (↑(HopfAlgebras.PTree.treeFactorialList ts))⁻¹

The graded cut identity: the sum of inverse tree factorials over the cut terms of an ordered forest whose trunk has k vertices equals C(|ω|, k) / ω! (arXiv:2507.21006 background; Hairer-Lubich-Wanner III.1).

theorem BSeries.PTree.flow_identity (R : Type u) [Field R] [CharZero R] (h h' : R) (ts : List HopfAlgebras.PTree) : (List.map (fun (t : HopfAlgebras.RootedForest × HopfAlgebras.RootedForest) => h ^ t.1.order * (↑t.1.treeFactorial)⁻¹ * (h' ^ t.2.order * (↑t.2.treeFactorial)⁻¹)) (HopfAlgebras.PTree.coproductTermsList ts)).sum = (h + h') ^ HopfAlgebras.PTree.orderList ts * (↑(HopfAlgebras.PTree.treeFactorialList ts))⁻¹

The flow identity for cuts of ordered forests:

Σ_{cuts} h^{|P^c|}/P^c! · h'^{|R^c|}/R^c! = (h + h')^{|ω|} / ω!.

This is the combinatorial content of the composition law of exact flows, B_h ∘ B_{h'} = B_{h+h'}.