Symmetry-weighted pairing for GL ↔ CK duality

[foissy-typed-decorated-rooted-trees-2018] [grossman-larson-1989] [MCB25]

The pairing ⟨·, ·⟩ : H × H → R (where H = ConnesKreimer R (Nonplanar α)) realizes the duality between the Connes-Kreimer (CK) and Grossman-Larson (GL) Hopf algebras on the shared carrier. By Foissy 2018 (hal-01924416, §4.2), GL associativity ⇔ Δ^c coassociativity via the pairing — the Δ^c proof in R.7 transports the GL proof from GrossmanLarson.lean (R.5) through this duality.

MCB targets

The pairing is the bridge that makes the GL framework (GrossmanLarson.lean) usable to prove MCB's coassociativity claims:

• Lemma 1.2.10 (Δ^c bialgebra): coassoc transported via this pairing from GrossmanLarson.product_assoc.
• Lemma 1.7.3 (Insertion Lie ↔ primitives in H^∨): the dual Lie bracket on H^∨ is induced by this pairing; MCB's binary ◁_e (Def 1.7.1) is its binary specialization after 1 − α quotient.
• Δ^d (MCB Def 1.2.5) and Δ^ρ (Lemma 1.2.11): same pairing framework, different extraction policies. See memory/project_mcb_unification_rationale.md.

The pairing (Foissy 2018 §4.2)

For nonplanar rooted trees, the pairing on basis elements is symmetry-weighted:

⟨of' F, of' G⟩ = if F = G then |Aut(F)| else 0

where Aut(F) is the automorphism group of F as a multiset of trees (i.e., the product ∏_T |Aut(T)|^{m_T(F)} · m_T(F)! over distinct trees T with multiplicities m_T(F), where Aut(T) is the rooted- tree automorphism group of T).

Bilinearly extended to H →ₗ[R] H →ₗ[R] R. The pairing is symmetric (because the underlying ⟨·,·⟩ on basis is symmetric in F, G) and non-degenerate (the basis vectors are mutually orthogonal with non-zero diagonal, so no non-zero element pairs to 0 with all others — at least when R is characteristic-0; over ℤ there are torsion subtleties when |Aut(F)| = 0 or non-invertible).

Status

[UPSTREAM] candidate. Sorry-free, including pairing_nondegenerate. The aut-cardinality substrate Nonplanar.autCard / Nonplanar.forestAutCard lives in Linglib/Core/Combinatorics/RootedTree/Aut.lean (re-exported here as treeAutCard / forestAutCard), also sorry-free.

Automorphism count

The cardinality of the automorphism group of a rooted nonplanar tree (or forest) is the symmetry weight in the pairing. The actual substrate for these is in Linglib/Core/Combinatorics/RootedTree/Aut.lean — re-exported here under the GrossmanLarson namespace for use in the pairing.

noncomputable def RootedTree.GrossmanLarson.treeAutCard {α : Type u_2} (t : Nonplanar α) : ℕ

Re-export Nonplanar.autCard for use in the pairing.

Equations

• RootedTree.GrossmanLarson.treeAutCard t = t.autCard

noncomputable def RootedTree.GrossmanLarson.forestAutCard {α : Type u_2} (F : Forest (Nonplanar α)) : ℕ

Re-export Nonplanar.forestAutCard for use in the pairing.

Equations

• RootedTree.GrossmanLarson.forestAutCard F = RootedTree.Nonplanar.forestAutCard F

The bilinear pairing

noncomputable def RootedTree.GrossmanLarson.pairing {R : Type u_1} [CommSemiring R] {α : Type u_2} : ConnesKreimer R (Nonplanar α) →ₗ[R] ConnesKreimer R (Nonplanar α) →ₗ[R] R

The symmetry-weighted pairing ⟨·, ·⟩ : H × H → R. On basis elements, ⟨of' F, of' G⟩ = if F = G then forestAutCard F else 0 (in R, via Nat.cast). Bilinearly extended, transported from the forest-basis pairingAux through ConnesKreimer.toFinsuppAlgEquiv.

Equations

• RootedTree.GrossmanLarson.pairing = RootedTree.GrossmanLarson.pairingAux✝.compl₁₂ RootedTree.ConnesKreimer.toFinsuppAlgEquiv.toLinearMap RootedTree.ConnesKreimer.toFinsuppAlgEquiv.toLinearMap

@[simp]

theorem RootedTree.GrossmanLarson.pairing_of'_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (F G : Forest (Nonplanar α)) : (pairing (ConnesKreimer.of' F)) (ConnesKreimer.of' G) = if F = G then ↑(forestAutCard F) else 0

theorem RootedTree.GrossmanLarson.pairing_symm {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y : ConnesKreimer R (Nonplanar α)) : (pairing x) y = (pairing y) x

The pairing is symmetric. Reduces by bilinearity to the basis case, where pairing_of'_of' shows both sides are if F = G then forestAutCard F else 0 — same value (the F = G case forces it).

@[simp]

theorem RootedTree.GrossmanLarson.pairing_zero_left {R : Type u_1} [CommSemiring R] {α : Type u_2} (y : ConnesKreimer R (Nonplanar α)) : (pairing 0) y = 0

The pairing vanishes on 0. Free from linearity.

@[simp]

theorem RootedTree.GrossmanLarson.pairing_zero_right {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (Nonplanar α)) : (pairing x) 0 = 0

The pairing vanishes on 0 (right).

theorem RootedTree.GrossmanLarson.pairing_apply_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (Nonplanar α)) (G : Forest (Nonplanar α)) : (pairing x) (ConnesKreimer.of' G) = x.coeff G * ↑(forestAutCard G)

Each pairing against a basis element of' G extracts the coefficient of G in x, weighted by forestAutCard G. Proof: reduce to basis via Finsupp.induction_linear on x, then pairing_of'_of'.

theorem RootedTree.GrossmanLarson.pairing_nondegenerate {R : Type u_1} [CommSemiring R] {α : Type u_2} [CharZero R] [NoZeroDivisors R] (x : ConnesKreimer R (Nonplanar α)) (h : ∀ (y : ConnesKreimer R (Nonplanar α)), (pairing x) y = 0) : x = 0

Non-degeneracy of the pairing over CharZero R with no zero divisors. If pairing x y = 0 for all y, then x = 0. Uses pairing_apply_of' (coefficient extraction) + forestAutCard_pos (positivity) + Nat.cast_ne_zero (CharZero R has no Nat-cast torsion)

• mul_eq_zero (NoZeroDivisors R).

Holds for any commutative ring with characteristic 0 and no zero divisors (e.g. ℤ, ℚ, ℝ, ℂ, any field of char 0).

Product rule

Pairing against a CK product decomposes over the two-sided sub-multiset splits of the first argument (Multiset.antidiagonal) — the symmetry-weighted pairing turns CK multiplication into the split coproduct. The combinatorial heart is the multinomial identity Nonplanar.forestAutCard_add (Aut.lean). Computationally validated (scratch/validate_duality.lean, V2 battery).

theorem RootedTree.GrossmanLarson.pairing_of'_mul_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (W C₁ C₂ : Forest (Nonplanar α)) : (pairing (ConnesKreimer.of' W)) (ConnesKreimer.of' C₁ * ConnesKreimer.of' C₂) = (Multiset.map (fun (p : Multiset (Nonplanar α) × Multiset (Nonplanar α)) => (pairing (ConnesKreimer.of' p.1)) (ConnesKreimer.of' C₁) * (pairing (ConnesKreimer.of' p.2)) (ConnesKreimer.of' C₂)) (Multiset.antidiagonal W)).sum

Pairing product rule (basis form): ⟨W, C₁ · C₂⟩ = Σ_{W = W₁ + W₂} ⟨W₁, C₁⟩ · ⟨W₂, C₂⟩.

Only the split (C₁, C₂) survives the diagonal pairing, with multiplicity count (C₁,C₂) (antidiagonal W); the autCard weights recombine via Nonplanar.forestAutCard_add.

theorem RootedTree.GrossmanLarson.pairing_of'_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} (W : Forest (Nonplanar α)) (z₁ z₂ : ConnesKreimer R (Nonplanar α)) : (pairing (ConnesKreimer.of' W)) (z₁ * z₂) = (Multiset.map (fun (p : Multiset (Nonplanar α) × Multiset (Nonplanar α)) => (pairing (ConnesKreimer.of' p.1)) z₁ * (pairing (ConnesKreimer.of' p.2)) z₂) (Multiset.antidiagonal W)).sum

Pairing product rule (bilinear form): pairing a basis vector against a product decomposes over the antidiagonal splits of the basis forest. Bilinear extension of pairing_of'_mul_of'.