FormSet operators FS^(k) — MCB Def 1.16.1 #
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:
Δ_Pis the primitive coproduct:Δ_P(T) = T ⊗ 1 + 1 ⊗ Tfor 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) ⊗ idwhereγ_(k)(F) = Fif F has exactlykcomponents, else 0.B(MCB Def 1.3.2): the grafting operator F ↦ tree with fresh root. In our typed substrate this is exactlybPlusLin afromPruningNonplanar.lean(parameterized by a root labela).⊔is the workspace product (CK multiplication on forests).
What FS^(k) does #
For F = T₁ ⊔ … ⊔ T_n:
Δ_P(F)decomposes into2^ntensor terms (each T_i is primitive, so each Δ_P(T_i) = T_i ⊗ 1 + 1 ⊗ T_i has 2 summands).Π_(k)selects only the terms whose left channel has exactlykcomponents.B ⊗ idgrafts thosekcomponents into a new tree with a fresh root (labeledain our typed setting).⊔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_kmapsT_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.
§1: The grafting operator B (MCB Def 1.3.2) #
In our typed Nonplanar α substrate, B needs a root label parameter.
This is exactly the existing bPlusLin a (Hochschild 1-cocycle for
Δ^ρ; reused here as the FormSet grafting operator).
The grafting operator B (MCB Def 1.3.2): create a new tree
with a fresh root labeled a and the forest F as children.
Identical to bPlus a F = Nonplanar.node a F; this name highlights
the FormSet usage.
Equations
Instances For
The grafting operator linearly extended: re-export bPlusLin
from PruningNonplanar.lean under the FormSet-flavored name.
Instances For
§2: 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.
Per-tree primitive coproduct: T ↦ ofTree T ⊗ 1 + 1 ⊗ ofTree T.
Equations
- RootedTree.ConnesKreimer.primTensor T = RootedTree.ConnesKreimer.ofTree T ⊗ₜ[R] 1 + 1 ⊗ₜ[R] RootedTree.ConnesKreimer.ofTree T
Instances For
Forest-level primitive coproduct: F ↦ ∏_{T ∈ F} primTensor T.
Equations
- RootedTree.ConnesKreimer.comulPrimForest F = (Multiset.map RootedTree.ConnesKreimer.primTensor F).prod
Instances For
comulPrimForest as a Multiplicative (Forest (Nonplanar α)) →* ….
Equations
- One or more equations did not get rendered due to their size.
Instances For
The primitive coproduct Δ_P as an algebra hom.
Equations
Instances For
§3: 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.
The k-component projection γ_(k) on ConnesKreimer R (Nonplanar α):
on basis of' F, returns of' F if F.card = k, else 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
§4: 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).
The CK multiplication as a LinearMap from H ⊗ H → H.
Equations
- RootedTree.ConnesKreimer.mulLin = LinearMap.mul' R (RootedTree.ConnesKreimer R (RootedTree.Nonplanar α))
Instances For
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.