Prefix decomposition of branch integrals

A single unfolding identity: the auxiliary branch integral of an ordered growth, with its mixed-partial integrand, is the sum over admissible next edges of prefixed ordered-simplex integrals. This is the shape in which the local recursion step behind the BKAR forest interpolation formula (see BKAR.Formula) consumes the branch integral.

theorem BKAR.Forest.ActiveTerminalBranchData.branchIntegralAux_mixedPartialList_eq_sum_prefixed_orderedSimplexIntegralAux {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (pref : List (Edge V)) (prefixTs : List ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegralAux top (F.paramsOfOrder pref prefixTs) (mixedPartialList pref.reverse ρ) = ∑ e ∈ F.activeEdges.attach, orderedSimplexIntegralAux top (data.growth e).order fun (ts : List ℝ) => mixedPartialList (pref ++ (data.growth e).order).reverse ρ ((data.growth e).terminal.standardInterp ((data.growth e).terminal.paramsOfOrder (pref ++ (data.growth e).order) (prefixTs ++ ts)))

At a general recursion node, the selected terminal branch sum is a finite sum of ordered simplices whose edge order is the accumulated prefix followed by the selected terminal growth order.