The pairing product rule for the Grossman-Larson product #

[Foi02] [OG08]

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 Nonplanar.insertionMultiset_antidiagonal (PreLie/InsertionNonplanar.lean) with the pairing product rule pairing_of'_mul (GrossmanLarson/Pairing.lean); substrate for the GL/CK duality theorem pairing_gl_eq_pairing_coproduct_Rho (Coproduct/PruningDuality.lean).

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

Generic sum/product plumbing #

quadBind (from dev_quad.lean) #

The product index multiset #

The index identity #

The fused product rule for the GL product #

source

theorem GrossmanLarson.pairing_product_of'_mul_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (A B C₁ C₂ : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) :

(pairing ((product (ConnesKreimer.of' A)) (ConnesKreimer.of' B))) (ConnesKreimer.of' C₁ * ConnesKreimer.of' C₂) = (Multiset.map (fun (pq : (Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.Nonplanar α)) × Multiset (RoseTree.Nonplanar α) × Multiset (RoseTree.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.