Group the actual Leibniz terms by their coefficient derivative order.

theorem AVenhance.Infra.Section4.IteratesWordGrouping.iterate_list_sum_group_orders (P : List (List (Fin 2) × List (Fin 2))) (n : ℕ) (f : ℕ → ℝ) (hP : ∀ p ∈ P, p.1.length ≤ n) : (List.map (fun (p : List (Fin 2) × List (Fin 2)) => f p.1.length) P).sum = ∑ j ∈ Finset.range (n + 1), ↑(List.countP (fun (p : List (Fin 2) × List (Fin 2)) => p.1.length == j) P) * f j

theorem AVenhance.Infra.Section4.iterateSpatialSplits_sum_by_order (w : List (Fin 2)) (f : ℕ → ℝ) : (List.map (fun (p : List (Fin 2) × List (Fin 2)) => f p.1.length) (iterateSpatialSplits w)).sum = ∑ j ∈ Finset.range (w.length + 1), ↑(w.length.choose j) * f j

Exact binomial grouping, valid for any real weights and any ordered word.

theorem AVenhance.Infra.Section4.iterateSpatialSplits_sum_by_two_orders (w : List (Fin 2)) (f : ℕ → ℕ → ℝ) : (List.map (fun (p : List (Fin 2) × List (Fin 2)) => f p.1.length p.2.length) (iterateSpatialSplits w)).sum = ∑ j ∈ Finset.range (w.length + 1), ↑(w.length.choose j) * f j (w.length - j)

Both factor orders can be grouped: the scalar order is n minus the coefficient order, by the proved ordered-split identity.