Basis-level substrate for the Grossman-Larson product #
[OG08] [foissy-typed-decorated-rooted-trees-2018]
Combinatorial substrate connecting the Grossman-Larson product on
ConnesKreimer R (Nonplanar α) to Nonplanar.insertionMultiset (NIM):
host distributivity, single-guest associativity, representative
invariance, and the powerset sum forms consumed by the associativity
proof in GrossmanLarsonMonoid.lean (which derives mul_assoc from the
abstract Oudom-Guin ★-associativity via the ckIsoSymmetricAlgebra
bridge).
Main results #
Nonplanar.insertionMultiset_add_host(Prop 2.7.iii substrate): NIM into a disjoint-union host decomposes over guest partitions.Nonplanar.insertionMultiset_eq_of_reps: NIM computes on anyRoseTree-level representatives.Nonplanar.insertionMultiset_singleton_assoc: iterated single-guest grafting equals simultaneous grafting plus guest-nested grafting.insertion_mul_distrib(Prop 2.7.iii of [OG08] at basis level).product_of'_sum_form/mul_of'_sum_form/lhs_quadruple_form/rhs_quintuple_form: powerset sum forms of (iterated) GL products.
The deprecated direct combinatorial route to associativity (the A3.3
campaign: insertionMultiset_assoc, insertion_assoc_shuffled, the
Lemma-2.10 chain) was deleted on 2026-06-12 when the bridge route
closed; see GrossmanLarsonMonoid.lean.
[UPSTREAM] candidate (jointly with the OudomGuinCirc layer).
§1: Prop 2.7.iii — ∘ distributes over disjoint union via shuffle Δ #
The shuffle coproduct decomposition on each forest argument C is realized
explicitly as the sum over C.powerset of the partition (C₁, C - C₁).
The proof of Prop 2.7.iii at the GL/CK level reduces to a combinatorial
identity on Nonplanar.insertionMultiset (= NIM), which we state
separately and prove by descent from the RoseTree-level insertionForest.
Deep substrate: multi-graft into a disjoint union of host forests
decomposes as a Multiset.bind over guest partitions. This is the
combinatorial heart of Prop 2.7.iii at the basis level.
NIM(A + B, C) = Σ_{C₁ ⊆ C} {X_A + X_B : X_A ∈ NIM(A, C₁), X_B ∈ NIM(B, C-C₁)}
Proved via descent through RoseTree.Pathed.hostBucketSum and the powerset
bridge RoseTree.Pathed.listChoices_bridge_powerset_paired, plus
insertionForest_msform_invariance_guests to bridge RoseTree-level guests with
canonical Quotient.out representatives.
Representative invariance for NIM: Nonplanar.insertionMultiset F G
can be computed on ANY RoseTree-level representative lists hosts, guests
whose mk-image multisets are F and G respectively — not just the
canonical toList.map Quotient.out reps.
This is the workhorse for descents that need to swap canonical reps for
a convenient RoseTree-level list (e.g. Q.out v :: B.toList.map Q.out standing
in for (B + {v}).toList.map Q.out).
Deep substrate: NIM-level singleton-guest associativity.
(NIM A B).bind (X ↦ NIM X {v}) = NIM A (B + {v}) + (NIM B {v}).bind (X' ↦ NIM A X')
Proved by descent from the raw RoseTree-level identity
RoseTree.Pathed.insertionForest_bind_singleton. The descent uses the
representative-invariance lemma
Nonplanar.insertionMultiset_eq_of_reps per-output to swap NIM applied
to a RoseTree-level output msform L for the RoseTree-level engine applied to L.
Prop 2.7.iii (Oudom-Guin 2004): for basis forests A, B, C, the
multi-graft of (A · B) (disjoint-union product) into C distributes
as a sum over partitions of C, with each part inserted into A vs B
independently.
(A · B) ∘ C = Σ_{C₁ ⊆ C} (A ∘ C₁) · (B ∘ (C - C₁))
Proved from insertionMultiset_add_host + bilinearity of CK's
disjoint-union product ·.
§3: Cocommutativity of the shuffle sum #
The sum-over-powerset is symmetric under the partition swap
(C₁, C - C₁) ↔ (C - C₁, C₁), since Multiset.powerset is closed under
complement. This is the "cocommutativity of Δ" component of Lemma 2.10.
Cocommutativity of shuffle Δ: a sum over C.powerset is invariant
under the partition swap.
Specifically: Σ_{C₁ ⊆ C} f(C₁, C - C₁) = Σ_{C₁ ⊆ C} f(C - C₁, C₁)
where the implicit complementation is a bijection on C.powerset.
Used in Lemma 2.10's chain to reindex one of the three triple-partition
sums for B_(2) ∘ C matching.
§4: Closing mul_assoc_basis via Oudom-Guin Lemma 2.10's chain #
The 6-line algebraic chain:
(A * B) * C = (((A ∘ B_(1)) B_(2)) ∘ C_(1)) C_(2) — def of *
= ((A ∘ B_(1)) ∘ C_(1))(B_(2) ∘ C_(2)) C_(3) — insertion_mul_distrib
= (A ∘ ((B_(1) ∘ C_(1)) C_(2)))(B_(2) ∘ C_(3)) C_(4) — insertion_assoc_shuffled
= (A ∘ ((B_(1) ∘ C_(1)) C_(3)))(B_(2) ∘ C_(2)) C_(4) — powerset_partition_swap (on C-trio)
= A * ((B ∘ C_(1)) C_(2)) — def of *
= A * (B * C)
The trio re-indexing on C uses powerset_partition_swap to swap the
"goes into B_(1)" piece of C with the "goes into B_(2)" piece, which
re-pairs the four-way C-partition into the right form for the RHS.
§4a: Generalized building blocks #
The chain manipulates GL elements that are themselves sums of basis
vectors (the output of insertion, a sum-over-partition, ...). To keep
the chain's rewrites compositional, we lift two basis-form identities to
LinearMap-general form via standard linearity arguments.
The lifts are routine ConnesKreimer.induction_linear (zero / additive /
scalar-of-basis) reductions to the basis form.
Push X * of' G to the explicit powerset sum form for ANY X.
Generalization of of'_mul_of' + productForest unfolding to non-basis
LEFT factor.
Stated via product (the bilinear underlying map of *) to avoid
Finsupp/GrossmanLarson type-alias mismatches in the induction.
Corollary: mul_of'_sum_form (the * form, given by mul_def).
LEFT-form distributivity of * over Multiset.sum:
(of' A) * (Σ s) = Σ ((of' A) * s_i). The Grossman-Larson product
* is bilinear (via product : GL →ₗ[R] GL →ₗ[R] GL), so pushing
through Multiset.sum is straightforward — the Mul instance
rewires * as product, and product (of' A) is a LinearMap.
Mirror of insertion_sum_right but for the GL product. Used in
Lemma 2.10's chain to expand (of' A) * (B * C) after substituting
B * C as a sum-form.
insertion distributes over a Multiset.sum in its first argument
(since the LinearMap on the first arg pushes through Multiset.sum).
insertion distributes over a Multiset.sum in its second argument.
Generalized insertion_mul_distrib: the bracketed LEFT factor of
μ(X, of' Y) may be any GL element. Reduces by linearity in X to
the basis case insertion_mul_distrib.
§4b: Lemma 2.10's chain — mul_assoc_basis proved #
The chain expands (of'A * of'B) * of'C step-by-step:
(of'A * of'B) * of'C = productForest (of'A * of'B) C(bymul_of')of'A * of'B = productForest (of'A) B(byof'_mul_of'); expand both levels ofproductForestto nested sums.- Apply
insertion_mul_distrib_gento split eachinsertion(μ(...), of'C₁)along a sub-partitionC₂ ⊆ C₁. - Apply
insertion_assoc_shuffled(basis form is enough — the LEFT factor at this point isinsertion (of' A) (of' B₁), which only becomes a sum after the assoc-rewrite ofinsertion_assoc_shuffled_gen, but here we're at fixedB₁so the basis form applies). - After all these rewrites, the LHS has a four-way C-partition:
C₂, C₁ - C₂, C - C₁plus another implicitB-derived split. - Re-index the C-partition via
powerset_partition_swap. - Similarly expand the RHS, observe that after
powerset_partition_swapthe two expressions are syntactically the same multiset sum.
Helpers for the chain proof #
Each helper expresses one stage of the LHS or RHS expansion.
Basis-form rewrite: (of' F₁) * (of' F₂) as a sum of basis vectors of' (X + (F₂ - B₁))
indexed by B₁ ⊆ F₂ and X ∈ NIM F₁ B₁. Uses mul_of'_sum_form then
insertion_of'_of' and of'_add to collapse to a forest sum.
Basis-form rewrite of LHS ((of' F₁) * of' F₂) * of' F₃ as a quadruple-bind
sum. The outer two binds come from the Foissy-form expansion; the inner
two come from insertionMultiset_add_host applied to NIM (X + (F₂-B₁)) C₁.
Public: consumed by GrossmanLarsonMonoid.lean to identify the
associativity LHS / RHS at the multiset-indexing level (R-generic).
Basis-form rewrite of RHS (of' F₁) * ((of' F₂) * of' F₃) as a quintuple-bind
sum (after applying Multiset.powerset_add to (Z + (F₃-C₁')).powerset):
Σ_{C₁' ⊆ F₃, Z ∈ NIM F₂ C₁', P_Z ⊆ Z, P_F ⊆ F₃-C₁', W ∈ NIM F₁ (P_Z+P_F)} of' (W + (Z - P_Z) + ((F₃-C₁') - P_F))
Public: consumed by GrossmanLarsonMonoid.lean, paired with
lhs_quadruple_form to derive R-generic associativity.