Used by Pair, forestCutsP, dcLHSP, dcRHSP, dcForestLHSP, dcForestRHSP, proj3, forestCutsP_cons, forestCutsP_add, Triple, dcForestLHSP_eq_bind, dcForestRHSP_eq_bind, dcForestLHSP_cons, dcForestRHSP_cons, coassFP_of_components, Cl, treeCutsP_node, dcLHSP_node, dcRHSP_node, clconv, clconv_bind, clconv_unit_left, clconv_unit_right, clconv_assoc, proj3L, proj3L_add, dcl, dcr, dclN_eq, dcrN_eq, dclN_clconv, dcrN_clconv, proj3L_list_wrap, dcl_INH_wrap, dcr_nonEW_wrap, dcl_cons, dcr_cons
Docs / Syntax / Minimalist / Workspace / Coproduct / DoubleCut
Double cuts of rose trees
import Linglib.Syntax.Minimalist.Workspace.Coproduct.DoubleCut · namespace DoubleCut
Both composites (Δ^c ⊗ id) ∘ Δ^c and (id ⊗ Δ^c) ∘ Δ^c enumerate the pairs of nested admissible
cuts of a tree, the second cut taken in the crown or in the trunk of the first. For a coherent
trace encoder the two enumerations agree up to the order of children. This file proves the
agreement on rose trees, where the cut enumeration recurses structurally, and Trace.lean
descends it to UnorderedTree, where it is the coassociativity of the coproduct Δ^c of
Marcolli, Chomsky and Berwick (their Lemma 1.2.10, p. 37).
Main results
DoubleCut.coassT: the two double-cut enumerations of a tree agree after projection.DoubleCut.coassL,DoubleCut.coassA: the same for a list of children and for one child;coassAis where trace coherence reconciles the marker a deeper cut writes on a trunk.DoubleCut.dclN_clconv,DoubleCut.dcrN_clconv: the two second cuts are multiplicative over the convolutionclconvof the cuts of a list of children.
References
- Marcolli et al. 2025, Mathematical Structure of Syntactic Merge: An Algebraic Model for Generative Linguistics formalized
- Foissy , An introduction to Hopf algebras of trees
Declarations
RoseTree tree-cut enumerator (crown forest, trunk forest).
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) :
Multiset (Pair (α ⊕ β))
- treeCutsP τ t = ({t}, 0) ::ₘ Multiset.map (fun (p : Multiset (RoseTree (α ⊕ β)) × RoseTree (α ⊕ β)) => (p.1, {p.2})) (ConnesKreimer.cutSummandsCP τ t)
Built from
Used by forestCutsP, forestCutsP_cons, forestCutsP_singleton, dcLHSP_eq_bind, dcRHSP_eq_bind, treeCutsP_node, dcRHSP_node
Forest-cut enumerator: convolution over the component trees.
- forestCutsP τ F = Multiset.foldr Multiset.conv {(0, 0)} (Multiset.map (treeCutsP τ) F)
Built from , ,
Used by forestCutsP_zero, forestCutsP_cons, forestCutsP_singleton, forestCutsP_add, hL, hR, dcForestLHSP_eq_bind, dcForestRHSP_eq_bind, dcLHSP_node, dcl, dclN_eq, dcl_cons
LHS double-cut: re-cut the crown.
The definition is too large to print here; read it in the source.
Built from
Used by dcLHSP_eq_bind, dcForestLHSP_cons, coassFP_of_components, dcLHSP_node, coassT
RHS double-cut: re-cut the trunk.
The definition is too large to print here; read it in the source.
Built from
Used by dcRHSP_eq_bind, dcForestRHSP_cons, coassFP_of_components, dcRHSP_node, coassT
Forest double-cut LHS (outer is a forest cut).
The definition is too large to print here; read it in the source.
Built from
Used by dcForestLHSP_eq_bind, dcForestLHSP_cons, dcForestLHSP_zero, coassFP_of_components
The definition is too large to print here; read it in the source.
Built from
Used by dcForestRHSP_eq_bind, dcForestRHSP_cons, dcForestRHSP_zero, coassFP_of_components
Projection of a triple of planar forests to nonplanar (mod planar order).
{α : Type u_1} {β : Type u_2} (q : FP (α ⊕ β) × FP (α ⊕ β) × FP (α ⊕ β)) :
Multiset (UnorderedTree (α ⊕ β)) × Multiset (UnorderedTree (α ⊕ β)) × Multiset (UnorderedTree (α ⊕ β))
- proj3 q = (Multiset.map UnorderedTree.mk q.1, Multiset.map UnorderedTree.mk q.2.1, Multiset.map UnorderedTree.mk q.2.2)
Built from
Used by proj3_add, proj3_conv, coassFP_of_components, coassT
Basic recursions for forestCutsP
Built from
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) (F : FP (α ⊕ β)) :
forestCutsP τ (t ::ₘ F) = (treeCutsP τ t).conv (forestCutsP τ F)
Built from , ,
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (F G : FP (α ⊕ β)) :
forestCutsP τ (F + G) = (forestCutsP τ F).conv (forestCutsP τ G)
Built from ,
Multiplicativity machinery
proj3 is additive
The two second-cut maps are monoid homs
The left-hand second cut re-cuts the crown p.1, carrying the trunk p.2.
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (p : Pair (α ⊕ β)) :
Multiset (Triple (α ⊕ β))
- hL τ p = Multiset.map (fun (A12 : Pair (α ⊕ β)) => (A12.1, A12.2, p.2)) (forestCutsP τ p.1)
Built from , ,
Used by hL_hom, dcLHSP_eq_bind, dcForestLHSP_eq_bind
The right-hand second cut re-cuts the trunk p.2, carrying the crown p.1.
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (p : Pair (α ⊕ β)) :
Multiset (Triple (α ⊕ β))
- hR τ p = Multiset.map (fun (B12 : Pair (α ⊕ β)) => (p.1, B12.1, B12.2)) (forestCutsP τ p.2)
Built from , ,
Used by hR_hom, dcRHSP_eq_bind, dcForestRHSP_eq_bind
Double-cut enumerators as binds of hL/hR
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (F : FP (α ⊕ β)) :
dcForestLHSP τ F = (forestCutsP τ F).bind (hL τ)
Built from , , ,
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (F : FP (α ⊕ β)) :
dcForestRHSP τ F = (forestCutsP τ F).bind (hR τ)
Built from , , ,
Multiplicativity of the forest double-cut
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) (F : FP (α ⊕ β)) :
dcForestLHSP τ (t ::ₘ F) = (dcLHSP τ t).conv (dcForestLHSP τ F)
Built from , ,
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) (F : FP (α ⊕ β)) :
dcForestRHSP τ (t ::ₘ F) = (dcRHSP τ t).conv (dcForestRHSP τ F)
Built from , ,
Built from
Built from
Forest coassoc from per-component tree coassoc
Node-level reduction of the per-tree double cut
The children-list cut enumerator (with trace leaves in the remainder),
distinct from forestCutsP (deletion). treeCutsP/dcLHSP/dcRHSP of a
node a cs decompose over it.
Children-list cut enumerator: cutListSummandsG (extractC τ).
- Cl τ cs = ConnesKreimer.cutListSummandsG (ConnesKreimer.extractC τ) cs
Built from
Used by treeCutsP_node, dcLHSP_node, dcRHSP_node, Cl_nil, Cl_cons, Cl_append, dcrN_eq, Cl_singleton, dcl_INH_wrap, dcr_nonEW_wrap, dcr_cons, coassL
The cuts treeCutsP of a node are the full cut and the root-preserving cuts coming
from the children-list cut wrapped with node a.
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) :
treeCutsP τ (RoseTree.node a cs) = ({RoseTree.node a cs}, 0) ::ₘ Multiset.map (fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => (p.1, {RoseTree.node a p.2})) (Cl τ cs)
Built from , ,
The left-hand double cut of a node consists of the full-cut boundary triple, the "split-at-root" middle terms, and the genuine children-crown re-cuts.
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) :
dcLHSP τ (RoseTree.node a cs) = ({RoseTree.node a cs}, 0, 0) ::ₘ Multiset.map (fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => (p.1, {RoseTree.node a p.2}, 0)) (Cl τ cs) + (Cl τ cs).bind fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => Multiset.map (fun (c12 : Pair (α ⊕ β)) => (c12.1, c12.2, {RoseTree.node a p.2})) (forestCutsP τ p.1)
Built from , , , ,
The right-hand double cut of a node consists of the full-cut boundary triple and, for
each children-cut, the re-cuts of the trunk tree node a remainder.
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) :
dcRHSP τ (RoseTree.node a cs) = {({RoseTree.node a cs}, 0, 0)} + (Cl τ cs).bind fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => Multiset.map (fun (B12 : Pair (α ⊕ β)) => (p.1, B12.1, B12.2)) (treeCutsP τ (RoseTree.node a p.2))
Built from , , , ,
Children-list convolution clconv and Cl as a monoid hom
Cl τ = cutListSummandsG (extractC τ) is a monoid hom from (List, ++) to
(Multiset (Forest × List), clconv). clconv is the cons-combiner of
cutListSummandsG (forest add, list append) — a (non-commutative) monoid
with unit {(0, [])}.
The children-list cut combiner: add crown forests, append remainders.
The definition is too large to print here; read it in the source.
Built from
Used by clconv_bind, clconv_unit_left, clconv_unit_right, clconv_assoc, Cl_cons, Cl_append, dclN_clconv, dcrN_clconv
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) (ts : List (RoseTree (α ⊕ β))) :
Cl τ (t :: ts) = clconv (ConnesKreimer.augActionG (ConnesKreimer.extractC τ) t) (Cl τ ts)
Built from ,
The two double-cut maps and their clconv-multiplicativity (mod proj)
dcl/dcr are the children-list double-cut enumerators (re-cut crown via
forestCutsP, vs re-cut remainder via Cl). Projected through proj3L
(third component = remainder list → multiset of nonplanar trees), each is
multiplicative over clconv.
Projection of a (crown, mid, remainder-list) triple to nonplanar.
{α : Type u_1} {β : Type u_2} (q : FP (α ⊕ β) × FP (α ⊕ β) × List (RoseTree (α ⊕ β))) :
Multiset (UnorderedTree (α ⊕ β)) × Multiset (UnorderedTree (α ⊕ β)) × Multiset (UnorderedTree (α ⊕ β))
- proj3L q = (Multiset.map UnorderedTree.mk q.1, Multiset.map UnorderedTree.mk q.2.1, ↑(List.map UnorderedTree.mk q.2.2))
Built from
Used by proj3L_add, dclN_eq, dcrN_eq, dclN_clconv, dcrN_clconv, proj3L_list_wrap, dcl_INH_wrap, dcr_nonEW_wrap, coassL, coassA
LHS children-list double cut: re-cut crown p.1, keep remainder p.2.
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (S : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) :
- dcl τ S = S.bind fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => Multiset.map (fun (c12 : Pair (α ⊕ β)) => (c12.1, c12.2, p.2)) (forestCutsP τ p.1)
Built from , ,
Used by dclN_eq, dclN_clconv, dcl_INH_wrap, dcl_cons, coassL, coassA
RHS children-list double cut: keep crown p.1, re-cut remainder p.2.
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (S : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) :
The definition is too large to print here; read it in the source.
Built from
Used by dcrN_eq, dcrN_clconv, dcr_nonEW_wrap, dcr_cons, coassL, coassA
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (S T : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) :
Built from , , ,
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (S T : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) :
Built from , , ,
The children-list coassociativity engine
coassL: the root-free children-list coassoc (LLEM3), proved by induction
on the list using clconv-multiplicativity, the per-child coassA, and
the tail IH. coassA (per-child) reduces to coassL of the child's
children with TraceCoherent reconciling the extract-whole marker.
Children-list coassoc (coassL) and per-child coassoc
(coassA), proved by mutual structural recursion mirroring
cutListSummandsG/augActionG. coassL is the engine of the per-tree
node step; coassA is the coherence-using combinatorial core.
τ is trace-coherent on rose trees when τ of a cut trunk equals τ of the tree. The
descent of TraceCoherent (UnorderedTree) along UnorderedTree.mk.
- TraceCoherentP τ = ∀ (t : RoseTree (α ⊕ β)), ∀ p ∈ ConnesKreimer.cutSummandsCP τ t, τ p.2 = τ t
Children-list cut of a singleton list is the per-child augmented action.
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) :
Cl τ [t] = ConnesKreimer.augActionG (ConnesKreimer.extractC τ) t
Built from
Projecting a triple whose remainder is a singleton [node a' l] equals
nonplanar node a'-wrapping the projection with raw remainder l.
{α : Type u_1} {β : Type u_2} (a' : α ⊕ β) (x y : FP (α ⊕ β)) (l : List (RoseTree (α ⊕ β))) :
proj3L (x, y, [RoseTree.node a' l]) = ((proj3L (x, y, l)).1, (proj3L (x, y, l)).2.1, {UnorderedTree.node a' (proj3L (x, y, l)).2.2})
Built from ,
The [node a']-wrapped dcl of the children cut, projected, equals the
nonplanar node a'-wrap of the projected dcl.
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a' : α ⊕ β) (cs'' : List (RoseTree (α ⊕ β))) :
Multiset.map proj3L (dcl τ (Multiset.map (fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => (p.1, [RoseTree.node a' p.2])) (Cl τ cs''))) = Multiset.map (fun (z : Multiset (UnorderedTree (α ⊕ β)) × Multiset (UnorderedTree (α ⊕ β)) × Multiset (UnorderedTree (α ⊕ β))) => (z.1, z.2.1, {UnorderedTree.node a' z.2.2})) (Multiset.map proj3L (dcl τ (Cl τ cs'')))
Built from , , ,
The non-extract-whole part of the trunk re-cut, projected, equals the
nonplanar node a'-wrap of the projected dcr.
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a' : α ⊕ β) (cs'' : List (RoseTree (α ⊕ β))) :
Multiset.map proj3L ((Cl τ cs'').bind fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => Multiset.map (fun (p'' : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => (p.1, p''.1, [RoseTree.node a' p''.2])) (Cl τ p.2)) = Multiset.map (fun (z : Multiset (UnorderedTree (α ⊕ β)) × Multiset (UnorderedTree (α ⊕ β)) × Multiset (UnorderedTree (α ⊕ β))) => (z.1, z.2.1, {UnorderedTree.node a' z.2.2})) (Multiset.map proj3L (dcr τ (Cl τ cs'')))
Built from , , ,
dcl distributes over a cons outer cut.
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (F : FP (α ⊕ β)) (l : List (RoseTree (α ⊕ β))) (S : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) :
dcl τ ((F, l) ::ₘ S) = Multiset.map (fun (c12 : Pair (α ⊕ β)) => (c12.1, c12.2, l)) (forestCutsP τ F) + dcl τ S
Built from , , ,
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (hτ : TraceCoherentP τ) (cs : List (RoseTree (α ⊕ β))) :
Built from , , , ,
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (hτ : TraceCoherentP τ) (c : RoseTree (α ⊕ β)) :
Multiset.map proj3L (dcl τ (ConnesKreimer.augActionG (ConnesKreimer.extractC τ) c)) = Multiset.map proj3L (dcr τ (ConnesKreimer.augActionG (ConnesKreimer.extractC τ) c))
Built from , , ,
Per-tree coassoc coassT from coassL (node reduction + root wrap)
{α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (hτ : TraceCoherentP τ) (t : RoseTree (α ⊕ β)) :
Built from , , ,