Exact binomial grouping of positive velocity and stream coefficient jets.

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

Removing the unique principal split leaves precisely coefficient orders j+1, with their original binomial multiplicities.

theorem AVenhance.Infra.Section4.iterateSpatialSplits_positive_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) (List.filter (fun (p : List (Fin 2) × List (Fin 2)) => !p.1.isEmpty) (iterateSpatialSplits w))).sum = ∑ j ∈ Finset.range w.length, ↑(w.length.choose (j + 1)) * f (j + 1) (w.length - (j + 1))

Both word orders remain exact after removing the principal split.