The split coproduct side of GL/CK duality

[Foi02] [OG08]

Two combinatorial laws connecting the Grossman-Larson product to the sub-multiset ("split") decomposition of forests, the substrate for the GL/CK duality theorem pairing_gl_eq_pairing_coproduct_Rho (Coproduct/PruningDuality.lean):

• Nonplanar.insertionMultiset_antidiagonal — splits of a multi-graft output factor through splits of host and guests (each guest follows its host component). The multi-graft counterpart of insertionMultiset_add_host, from which it is proved by induction on the host.
• pairing_product_of'_mul_of' — the GL-product/CK-product duality at the pairing level: ⟨A ⋆ B, C₁ · C₂⟩ decomposes over independent splits of A and B. Combines the insertion split law with the pairing product rule pairing_of'_mul (GrossmanLarsonPairing.lean).

Both statements are computationally validated against the planar simulation harness (scratch/validate_duality.lean, V3/V3b batteries, exhaustive over forests of weight ≤ 3 plus duplicate-tree traps).

Helper lemmas

A few small multiset/insertion building blocks used by both targets below.

Split law for multi-graft outputs

theorem RootedTree.Nonplanar.insertionMultiset_antidiagonal {α : Type u_2} (A G : Forest (Nonplanar α)) : (insertionMultiset A G).bind Multiset.antidiagonal = (Multiset.antidiagonal A).bind fun (pa : Multiset (Nonplanar α) × Multiset (Nonplanar α)) => (Multiset.antidiagonal G).bind fun (pg : Multiset (Nonplanar α) × Multiset (Nonplanar α)) => insertionMultiset pa.1 pg.1 ×ˢ insertionMultiset pa.2 pg.2

Splits of an insertion output factor through splits of host and guests. Each component of a multi-graft output X ∈ NIM(A, G) is one host component of A carrying the guests grafted into it, so a sub-multiset split of X induces a split of A and a split of G (guests follow their host), and the correspondence is multiplicity-faithful:

Σ_{X ∈ NIM(A,G)} Σ_{X = X₁ + X₂} (X₁, X₂) = Σ_{A = A₁+A₂} Σ_{G = G₁+G₂} NIM(A₁,G₁) ×ˢ NIM(A₂,G₂).

Proved by induction on A from insertionMultiset_add_host (peeling one host tree; NIM({T}, G) outputs are singleton forests, whose antidiagonal is the trivial two-way split).

Generic sum/product plumbing

theorem RootedTree.GrossmanLarson.sum_map_product_mul {R : Type u_1} [CommSemiring R] {β : Type u_3} {γ : Type u_4} (s : Multiset β) (t : Multiset γ) (f : β → R) (g : γ → R) : (Multiset.map (fun (p : β × γ) => f p.1 * g p.2) (s ×ˢ t)).sum = (Multiset.map f s).sum * (Multiset.map g t).sum

Sum of a product-indexed multiset of products factors.

quadBind (from dev_quad.lean)

The product index multiset

The index identity

The fused product rule for the GL product

theorem RootedTree.GrossmanLarson.pairing_product_of'_mul_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (A B C₁ C₂ : Forest (Nonplanar α)) : (pairing ((product (ConnesKreimer.of' A)) (ConnesKreimer.of' B))) (ConnesKreimer.of' C₁ * ConnesKreimer.of' C₂) = (Multiset.map (fun (pq : (Multiset (Nonplanar α) × Multiset (Nonplanar α)) × Multiset (Nonplanar α) × Multiset (Nonplanar α)) => (pairing ((product (ConnesKreimer.of' pq.1.1)) (ConnesKreimer.of' pq.2.1))) (ConnesKreimer.of' C₁) * (pairing ((product (ConnesKreimer.of' pq.1.2)) (ConnesKreimer.of' pq.2.2))) (ConnesKreimer.of' C₂)) (Multiset.antidiagonal A ×ˢ Multiset.antidiagonal B)).sum

GL-product/CK-product pairing duality (basis form): pairing a GL product against a CK product decomposes over independent splits of the two GL factors:

⟨A ⋆ B, C₁ · C₂⟩ = Σ_{A = A₁+A₂} Σ_{B = B₁+B₂} ⟨A₁ ⋆ B₁, C₁⟩ · ⟨A₂ ⋆ B₂, C₂⟩.

This is the multiplicative-structure compatibility making the GL basis dual to the CK polynomial algebra: combines pairing_of'_mul (pairing product rule, one application per output forest of A ⋆ B) with insertionMultiset_antidiagonal (routing splits of grafted outputs) and the powerset/antidiagonal bookkeeping for the non-grafted guest components.

Proof: reduce both sides to sums of the diagonal pairing over the index multiset productIdx; the multiset backbone is productIdx_mul_split, whose combinatorial heart is the middle-four interchange quadBind_middle_swap.