Dyson-Schwinger equations on ConnesKreimer R (Nonplanar α) — MCB §1.17

[MCB25]

MCB §1.17 ("Merge and Combinatorial Recursions in Physics") draws a structural parallel between two recursive equations:

• Eq 1.17.1 (Hochschild 1-cocycle): for the deletion-style coproduct Δ^ρ and the grafting operator B+_a, Δ^ρ ∘ B+_a = B+_a ⊗ 1 + (id ⊗ B+_a) ∘ Δ^ρ. This is the central algebraic property of B+_a that makes the Connes-Kreimer construction work.
• Eq 1.17.2 (combinatorial Dyson-Schwinger in physics): X = B+_a(P(X)), where P is a polynomial / linear operator on the Hopf algebra. The classical case P(X) = 1 + X² gives the famous Foissy / Bergbauer-Kreimer "ladder" trees of perturbative QFT.
• Eq 1.17.3 (Merge fixed-point): X = M(X, X), where M is the linguistic Merge operator on syntactic objects (also MCB §1.10 Prop 1.10.2). The book's claim is that this linguistic recursion has the same formal shape as Eq 1.17.2.

This file provides the algebraic substrate (Eq 1.17.1 + 1.17.2 + an algebraic quadratic DS analog of Eq 1.17.3). The fully linguistic Eq 1.17.3 (interpreted as a type-level recursion on SyntacticObject) belongs in Syntax/Minimalist/ — those Studies files consume this substrate.

B+ as Hochschild 1-cocycle for Δ^ρ (MCB Eq 1.17.1)

Already proven as comulTreeN_node_cocycle / comulAlgHomN_bPlusLin_cocycle in Coproduct/Pruning.lean; this file consumes those theorems directly.

The Dyson-Schwinger map and equation (MCB Eq 1.17.2)

For P : H →ₗ[R] H a linear self-map and a : α a root label, the Dyson-Schwinger map is

dsMap P a := bPlusLin a ∘ₗ P

A DS solution for (P, a) is an X : H satisfying X = dsMap P a X, equivalently X = B+_a(P(X)). The classical existence theorem (Foissy 2008) requires the degree-completion of H (formal power series in the grading variable) and is out of scope for this substrate file.

Algebraic analog of MCB Eq 1.17.3

The quadratic case X = B+_a(X * X) is the direct algebraic analog of MCB Eq 1.17.3. It is not literally X = M(X, X) (which is a type-level claim about SyntacticObject), but it captures the same recursion shape in the CK algebra.

Status

[UPSTREAM] candidate. Sorry-free. Pure substrate built on Pruning.lean (B+ + Δ^ρ).

The Dyson-Schwinger map and equation

For a linear endomorphism P : H →ₗ[R] H and a root label a : α, dsMap P a := bPlusLin a ∘ₗ P is the DS self-map.

noncomputable def ConnesKreimer.dsMap {R : Type u_1} [CommSemiring R] {α : Type u_2} (P : ConnesKreimer R (RoseTree.Nonplanar α) →ₗ[R] ConnesKreimer R (RoseTree.Nonplanar α)) (a : α) : ConnesKreimer R (RoseTree.Nonplanar α) →ₗ[R] ConnesKreimer R (RoseTree.Nonplanar α)

The Dyson-Schwinger map T_{P,a}(X) := B+_a(P(X)) for a linear operator P and root label a.

Equations

• ConnesKreimer.dsMap P a = ConnesKreimer.bPlusLin a ∘ₗ P

@[simp]

theorem ConnesKreimer.dsMap_apply {R : Type u_1} [CommSemiring R] {α : Type u_2} (P : ConnesKreimer R (RoseTree.Nonplanar α) →ₗ[R] ConnesKreimer R (RoseTree.Nonplanar α)) (a : α) (X : ConnesKreimer R (RoseTree.Nonplanar α)) : (dsMap P a) X = (bPlusLin a) (P X)

def ConnesKreimer.IsDSSolution {R : Type u_1} [CommSemiring R] {α : Type u_2} (P : ConnesKreimer R (RoseTree.Nonplanar α) →ₗ[R] ConnesKreimer R (RoseTree.Nonplanar α)) (a : α) (X : ConnesKreimer R (RoseTree.Nonplanar α)) : Prop

MCB Eq 1.17.2: an element X : H is a Dyson-Schwinger solution for the pair (P, a) if it is a fixed point of the DS map, i.e., X = B+_a(P(X)).

Equations

• ConnesKreimer.IsDSSolution P a X = (X = (ConnesKreimer.dsMap P a) X)

theorem ConnesKreimer.IsDSSolution.def {R : Type u_1} [CommSemiring R] {α : Type u_2} (P : ConnesKreimer R (RoseTree.Nonplanar α) →ₗ[R] ConnesKreimer R (RoseTree.Nonplanar α)) (a : α) (X : ConnesKreimer R (RoseTree.Nonplanar α)) : IsDSSolution P a X ↔ X = (bPlusLin a) (P X)

theorem ConnesKreimer.dsMap_add {R : Type u_1} [CommSemiring R] {α : Type u_2} (P Q : ConnesKreimer R (RoseTree.Nonplanar α) →ₗ[R] ConnesKreimer R (RoseTree.Nonplanar α)) (a : α) : dsMap (P + Q) a = dsMap P a + dsMap Q a

dsMap is additive in P.

theorem ConnesKreimer.dsMap_smul {R : Type u_1} [CommSemiring R] {α : Type u_2} (r : R) (P : ConnesKreimer R (RoseTree.Nonplanar α) →ₗ[R] ConnesKreimer R (RoseTree.Nonplanar α)) (a : α) : dsMap (r • P) a = r • dsMap P a

dsMap commutes with scalar multiplication.

@[simp]

theorem ConnesKreimer.dsMap_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) : dsMap 0 a = 0

dsMap is zero on the zero operator.

theorem ConnesKreimer.isDSSolution_zero_iff_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (X : ConnesKreimer R (RoseTree.Nonplanar α)) : IsDSSolution 0 a X ↔ X = 0

For the zero operator P = 0, the unique DS solution is X = 0 (since dsMap 0 a X = B+_a(0) = 0 for all X).

Quadratic Dyson-Schwinger

The equation X = B+_a(X * X) is the direct algebraic analog of MCB Eq 1.17.3 (X = M(X, X)). Not a dsMap instance — multiplication by X is bilinear, not linear, so this lives outside the linear DS framework.

The two-tree-product solution X = ofTree (Nonplanar.node a {T, T}) for a fixed T is structurally a "two-children-with-same-subtree" recursion.

def ConnesKreimer.IsQuadDSSolution {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (X : ConnesKreimer R (RoseTree.Nonplanar α)) : Prop

The quadratic Dyson-Schwinger predicate: X = B+_a(X * X). Algebraic analog of MCB Eq 1.17.3 X = M(X, X).

Equations

• ConnesKreimer.IsQuadDSSolution a X = (X = (ConnesKreimer.bPlusLin a) (X * X))

theorem ConnesKreimer.zero_isQuadDSSolution {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) : IsQuadDSSolution a 0

0 is trivially a quadratic-DS solution (since 0 * 0 = 0 and B+_a(0) = 0).

Sanity tests