Exact binomial multiplicities for ordered Leibniz expansions.

theorem AVenhance.Infra.Section4.IteratesWordMultiplicity.split_count_sum (P : List (List (Fin 2) × List (Fin 2))) (j : ℕ) : (List.map (fun (p : List (Fin 2) × List (Fin 2)) => if p.1.length = j then 1 else 0) P).sum = List.countP (fun (p : List (Fin 2) × List (Fin 2)) => p.1.length == j) P

theorem AVenhance.Infra.Section4.iterateSpatialSplits_count (w : List (Fin 2)) (j : ℕ) : List.countP (fun (p : List (Fin 2) × List (Fin 2)) => p.1.length == j) (iterateSpatialSplits w) = w.length.choose j

Grouping splits by coefficient derivative order gives the binomial coefficient; repeated coordinate letters retain their full multiplicity.