Documentation

Linglib.Core.Algebra.RootedTree.PreLie.OudomGuinBridgePairing

Phase D: Q5c via pairing nondegeneracy (OG-faithful route) #

[OG08] [foissy-typed-decorated-rooted-trees-2018]

This file implements OG paper Prop 3.2's proof strategy on the linglib substrate. The goal is:

gl_product_eq_oudomGuinStar_via_pairing : ckIso (X ★ Y) = unop (op (ckIso X) * op (ckIso Y))

i.e., the OG ★ on S(InsertionAlgebra α) transports under ckIsoSymmetricAlgebra to the Grossman-Larson product on ConnesKreimer ℤ (Nonplanar α).

Strategy #

By pairing nondegeneracy (pairing_nondegenerate over ℤ with [CharZero] [NoZeroDivisors]), it suffices to show

⟨ckIso(X ★ Y), z⟩ = ⟨unop (op (ckIso X) * op (ckIso Y)), z⟩ for all z.

For each z, this reduces — via the B+/B- adjoint (bMinusLin_pairing_adjoint) + the Phase C OG identity (bMinusLin_gl_mul) on the CK side, and OG's Prop 2.8.ii (ε of ★) on the S(L) side — to a recursion that bottoms out at ε(X) · ε(Y) for z = 1.

Inputs #

Status #

Skeleton only. Sub-proofs sorry-fenced for incremental closure.

ε is multiplicative for the GL product #

The cardinality preservation lemma Nonplanar.insertionMultiset_card_eq (every F' ∈ NIM(A, B) has |F'| = |A|) and its planar substrate RoseTree.Pathed.insertionForest_length now live in Linglib.Core.Combinatorics.RootedTree.Nonplanar.Insertion.

source
theorem RootedTree.GrossmanLarson.counit_gl_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq (Nonplanar α)] (x y : ConnesKreimer R (Nonplanar α)) :
ConnesKreimer.counit (op x * op y).unop = ConnesKreimer.counit x * ConnesKreimer.counit y

The counit ε on CK is multiplicative for the GL product. Bilinear extension of counit_gl_mul_basis.

Phase D's pairing-side recurrence #

source
theorem RootedTree.GrossmanLarson.pairing_apply_bPlus_gl_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (X Y z : ConnesKreimer R (Nonplanar α)) :
(pairing (op X * op Y).unop) ((ConnesKreimer.bPlusLin a) z) = ConnesKreimer.counit X * (pairing ((bMinusLin a) Y)) z + (pairing (op ((bMinusLin a) X) * op Y).unop) z

Phase D RHS recurrence: ⟨unop (op X * op Y), bPlusLin a z⟩ unfolds via B+/B- adjoint + Phase C bMinusLin_gl_mul.

Specifically: ⟨unop (op X * op Y), B+_a z⟩ = ε(X) · ⟨B-_a Y, z⟩ + ⟨unop (op (B-_a X) * op Y), z⟩.

Phase D main: Q5c via pairing nondegeneracy #

source
theorem RootedTree.GrossmanLarson.gl_product_eq_oudomGuinStar_via_pairing {α : Type u_2} [DecidableEq (Nonplanar α)] (X Y : SymmetricAlgebra ℤ (InsertionAlgebra α)) :
ckIsoSymmetricAlgebra (PreLie.OudomGuinCirc.oudomGuinStar X Y) = op (ckIsoSymmetricAlgebra X) * op (ckIsoSymmetricAlgebra Y)

Q5c via OG B+/B- duality: ckIso (X ★ Y) = unop (op (ckIso X) * op (ckIso Y)). OG paper §3.2 Prop 3.2's statement, restated here as the entry point for the pairing-route Phase D.

Closure note (2026-05-17): After Phase B+C+D substrates closed (Steps 1, 3, 4, 5), an audit revealed the pairing-route induction on z's B+ structure requires an LHS recurrence bMinusLin a (ckIso (X★Y)) = ε(ckIso X) • bMinusLin a (ckIso Y) + ckIso (B⁻_SL X ★ Y) — which is OG Prop 3.2 transported via ckIso, and equivalent to Q5c itself (circular without independent OG-side machinery).

The pairing route's strict advantage over the existing tprod-route (gl_product_eq_oudomGuinStar) was meant to be: bypass substrate 2 (the deprecated GL_product_split_mul_ι) by replacing combinatorial GL surgery with the linear-algebra pairing_nondegenerate + B+/B- duality. But the induction on z bottoms out at z = 1 (counit-side, closed via counit_gl_mul) and reduces the step case z = B+_a w to a recurrence on bMinusLin a (ckIso (X★Y)) that has no formula independent of Q5c.

Conclusion: delegate to the existing gl_product_eq_oudomGuinStar (still substrate-2-blocked). Phases A-D and their helpers (bMinusLin_gl_mul, counit_gl_mul, pairing_apply_bPlus_gl_mul) remain useful infrastructure for future approaches.