FormSet operators FS^(k) — MCB Def 1.16.1

[MCB25]

The FormSet operator family on workspaces, introduced in MCB §1.16 (book p. 141–146). FormSet is a structure-formation operation that groups subsets of workspace components into a single new structure via the grafting operator B, without unrolling its constituents to accessible terms (unlike Merge, which does both grafting and accessible-term extraction).

The MCB formula (Def 1.16.1, book p. 143)

FS^(k) = ⊔ ∘ (B ⊗ id) ∘ Π_(k) ∘ Δ_P

where:

• Δ_P is the primitive coproduct: Δ_P(T) = T ⊗ 1 + 1 ⊗ T for single trees, extended multiplicatively Δ_P(F) = ⊔_a Δ_P(T_a). Distinct from Δ^c / Δ^d / Δ^ρ (much simpler — coassoc + algebra-hom follow by construction, no Foissy axiom needed).
• Π_(k) = γ_(k) ⊗ id where γ_(k)(F) = F if F has exactly k components, else 0.
• B (MCB Def 1.3.2): the grafting operator F ↦ tree with fresh root. In our typed substrate this is exactly bPlusLin a from Pruning.lean (parameterized by a root label a).
• ⊔ is the workspace product (CK multiplication on forests).

What FS^(k) does

For F = T₁ ⊔ … ⊔ T_n:

1. Δ_P(F) decomposes into 2^n tensor terms (each T_i is primitive, so each Δ_P(T_i) = T_i ⊗ 1 + 1 ⊗ T_i has 2 summands).
2. Π_(k) selects only the terms whose left channel has exactly k components.
3. B ⊗ id grafts those k components into a new tree with a fresh root (labeled a in our typed setting).
4. ⊔ multiplies with the right-channel remainder.

The result is a workspace where some subset of k components has been "glued together" by the new root.

FS^(k) is NOT k-ary Merge (MCB §1.16.2)

• k-ary Merge M_k maps T_1, …, T_k ∈ T^(k) (k-ary syntactic objects) to a k-ary tree. FormSet maps binary workspaces to binary extended workspaces (the grouping is k-ary but the components stay binary).
• Merge can be undone by accessible-term extraction. FormSet's groupings are atomic for subsequent computation.

Status

[UPSTREAM] candidate (the comulPrim primitive coproduct + bPlusLin grafting are general Hopf-algebra-of-rooted-trees constructions, not linguistics-specific).

Lemma 1.16.5 (Δ^ω extends to extended workspaces F̃^R) deferred — needs a new "extended forest" type.

The primitive coproduct Δ_P (MCB Remark 1.16.2)

Δ_P treats every basis tree as primitive: Δ_P(T) = T ⊗ 1 + 1 ⊗ T. Extended multiplicatively to forests by Δ_P(F + G) = Δ_P(F) · Δ_P(G), so for F = ⊔_a T_a, Δ_P(F) = ∏_a (T_a ⊗ 1 + 1 ⊗ T_a).

Distinct from Δ^c / Δ^d / Δ^ρ (which extract subforests). Coassoc + algebra-hom by construction — no Foissy axiom needed.

noncomputable def ConnesKreimer.primTensor {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : RoseTree.Nonplanar α) : TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α))

Per-tree primitive coproduct: T ↦ ofTree T ⊗ 1 + 1 ⊗ ofTree T.

Equations

• ConnesKreimer.primTensor T = ConnesKreimer.ofTree T ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ConnesKreimer.ofTree T

noncomputable def ConnesKreimer.comulPrimForest {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) : TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α))

Forest-level primitive coproduct: F ↦ ∏_{T ∈ F} primTensor T.

Equations

• ConnesKreimer.comulPrimForest F = (Multiset.map ConnesKreimer.primTensor F).prod

@[simp]

theorem ConnesKreimer.comulPrimForest_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} : comulPrimForest 0 = 1

@[simp]

theorem ConnesKreimer.comulPrimForest_add {R : Type u_1} [CommSemiring R] {α : Type u_2} (F G : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) : comulPrimForest (F + G) = comulPrimForest F * comulPrimForest G

noncomputable def ConnesKreimer.comulPrimMonoidHom {R : Type u_1} [CommSemiring R] {α : Type u_2} : Multiplicative (RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) →* TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α))

comulPrimForest as a Multiplicative (Forest (Nonplanar α)) →* ….

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ConnesKreimer.comulPrim {R : Type u_1} [CommSemiring R] {α : Type u_2} : ConnesKreimer R (RoseTree.Nonplanar α) →ₐ[R] TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar α)) (ConnesKreimer R (RoseTree.Nonplanar α))

The primitive coproduct Δ_P as an algebra hom.

Equations

• ConnesKreimer.comulPrim = ConnesKreimer.lift ConnesKreimer.comulPrimMonoidHom

@[simp]

theorem ConnesKreimer.comulPrim_apply_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) : comulPrim (of' F) = comulPrimForest F

@[simp]

theorem ConnesKreimer.comulPrim_apply_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : RoseTree.Nonplanar α) : comulPrim (ofTree T) = ofTree T ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ofTree T

The k-component projection Π_(k) (MCB book p. 142)

γ_(k)(F) = F if F has exactly k components, else 0. Linearly extended to ConnesKreimer R (Nonplanar α). Then Π_(k) = γ_(k) ⊗ id on the left channel of the coproduct output.

noncomputable def ConnesKreimer.projectKComponent {R : Type u_1} [CommSemiring R] {α : Type u_2} (k : ℕ) : ConnesKreimer R (RoseTree.Nonplanar α) →ₗ[R] ConnesKreimer R (RoseTree.Nonplanar α)

The k-component projection γ_(k) on ConnesKreimer R (Nonplanar α): on basis of' F, returns of' F if F.card = k, else 0.

Equations

• ConnesKreimer.projectKComponent k = ConnesKreimer.linearLift fun (F : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) => if Multiset.card F = k then ConnesKreimer.of' F else 0

@[simp]

theorem ConnesKreimer.projectKComponent_of'_eq {R : Type u_1} [CommSemiring R] {α : Type u_2} (k : ℕ) (F : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) (h : Multiset.card F = k) : (projectKComponent k) (of' F) = of' F

@[simp]

theorem ConnesKreimer.projectKComponent_of'_ne {R : Type u_1} [CommSemiring R] {α : Type u_2} (k : ℕ) (F : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) (h : Multiset.card F ≠ k) : (projectKComponent k) (of' F) = 0

The FormSet operator FS^(k) (MCB Def 1.16.1)

FS^(k) = ⊔ ∘ (B ⊗ id) ∘ Π_(k) ∘ Δ_P where ⊔ is CK multiplication (lifted to a LinearMap from the tensor product) and the grafting operator B (MCB Def 1.3.2) is bPlusLin (Coproduct/Pruning.lean).

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

The CK multiplication as a LinearMap from H ⊗ H → H.

Equations

• ConnesKreimer.mulLin = LinearMap.mul' R (ConnesKreimer R (RoseTree.Nonplanar α))

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

MCB Def 1.16.1: the FormSet operator FS^(k) of arity k, parameterized by a root label a : α for the grafting operator B.

FS^(k)(F) = ⊔ ∘ (B ⊗ id) ∘ (Π_(k) ⊗ id) ∘ Δ_P (F)

The book uses k ≥ 3 (the binary/unary cases reduce to Merge); we don't enforce this here, since the formula is well-defined for any k ≥ 0.

Equations

• One or more equations did not get rendered due to their size.

Basic API + sanity tests

@[simp]

theorem ConnesKreimer.formSet_apply {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (k : ℕ) (x : ConnesKreimer R (RoseTree.Nonplanar α)) : (formSet a k) x = mulLin ((LinearMap.rTensor (ConnesKreimer R (RoseTree.Nonplanar α)) (bPlusLin a)) ((LinearMap.rTensor (ConnesKreimer R (RoseTree.Nonplanar α)) (projectKComponent k)) (comulPrim x)))