The Δ^c enumeration filters onto the Δ^ρ enumeration

On a Sum.inl-embedded tree, the Δ^c cut enumeration (cutSummandsCP) cuts at exactly the sites of the Δ^ρ enumeration (cutSummandsP): applying RoseTree.filterMap Sum.getLeft? to each Δ^c summand — which erases the trace placeholders — recovers the corresponding Δ^ρ summand, as an equality of multisets. Both sides are stated Option-valued (filtered on the left, embedded by some on the right), which keeps the maps total.

This is the combinatorial content of the Δ^d = Δ^ρ comparison ([MCB25] Lemma 1.3.10); the algebra layer (Core/Algebra/RootedTree/Coproduct/Deletion.lean) transports it through a cut-summand tensor builder.

Main results

• ConnesKreimer.cutSummandsCP_map_inl_filterMap — per-tree: filtered Δ^c summands of RoseTree.map Sum.inl t are the Δ^ρ summands of t.
• ConnesKreimer.cutListSummandsG_map_inl_filterMap, ConnesKreimer.augActionG_map_inl_filterMap — children-list and per-child companions of the mutual induction.

theorem ConnesKreimer.cutSummandsCP_map_inl_filterMap {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree α) : Multiset.map (Prod.map (Multiset.map (RoseTree.filterMap Sum.getLeft?)) (RoseTree.filterMap Sum.getLeft?)) (cutSummandsCP τ (RoseTree.map Sum.inl t)) = Multiset.map (Prod.map (Multiset.map some) some) (cutSummandsP t)

Filtering the Δ^c cut summands of an embedded tree yields the some-embedded Δ^ρ cut summands.

theorem ConnesKreimer.cutListSummandsG_map_inl_filterMap {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (cs : List (RoseTree α)) : Multiset.map (Prod.map (Multiset.map (RoseTree.filterMap Sum.getLeft?)) (RoseTree.filterMapList Sum.getLeft?)) (cutListSummandsG (extractC τ) (List.map (RoseTree.map Sum.inl) cs)) = Multiset.map (Prod.map (Multiset.map some) id) (cutListSummandsP cs)

Children-list companion of cutSummandsCP_map_inl_filterMap, with RoseTree.filterMapList on the remainder.

theorem ConnesKreimer.augActionG_map_inl_filterMap {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (c : RoseTree α) : Multiset.map (Prod.map (Multiset.map (RoseTree.filterMap Sum.getLeft?)) (RoseTree.filterMapList Sum.getLeft?)) (augActionG (extractC τ) (RoseTree.map Sum.inl c)) = Multiset.map (Prod.map (Multiset.map some) Option.toList) (augActionP c)

Per-child companion of cutSummandsCP_map_inl_filterMap for the augmented action, with the Δ^ρ Option remainder listed via Option.toList: the extract-whole branch filters to ({some c}, []), matching Δ^ρ's delete branch ({c}, none).