Marcolli, Chomsky and Berwick (2025): Mathematical Structure of Syntactic Merge

This file formalizes parts of Marcolli, Chomsky and Berwick's algebraic model of Merge.

Internal Merge (§1.4.4) is checked on the book's example, which raises the apple out of T = {was, {eaten, {the, apple}}}. The unit stage M_{T₂,1} splits T into the apple beside the quotient T/T₂, the composite with M_{T/T₂,T₂} merges the two (Proposition 1.4.2), and the step satisfies Minimal Yield under trace counting (Proposition 1.6.4).

The core computational structure of Merge (§1.10) is a fixed point. Proposition 1.10.2 works in V(𝔗), the free ℤ-module on the nonplanar binary trees with unlabelled leaves, graded by the number of leaves. It generates these trees by recursively solving X = 𝔐(X, X) over formal sums X = ∑ Xₗ, with the initial condition X₁ = x, and reads the integer coefficients of the solution as numbers of planar embeddings. Here V(𝔗) sits in the Connes–Kreimer algebra of unlabelled trees, Merge is the grafting operator after the disjoint union (Lemma 1.3.3), and a formal sum is a power series whose degree counts leaves. The sum of the planar binary trees, their planar structure forgotten, solves the equation (isMergeSolution_mergeSolution) and is its only solution (IsMergeSolution.eq). The coefficient of each tree is its number of planar embeddings (coeff_planarSum_succ), and the coefficients of Xₙ₊₁ sum to the Catalan number Cₙ (aeval_planarSum_succ). On syntactic objects, Lemma 1.3.3 is toCK_merge.

The book's worked examples of externalization are stated on the SyntacticObject carrier of the Minimalist substrate: the harmonic head-initial and head-final orders of a determiner–noun Merge, the head-side convention flipping the yield, and exocentric elimination, two saturated nouns determining no head and hence no order. The framework itself is the Syntax/Minimalist/ theory layer; the examples are kernel-checked against it.

FormSet (§1.16) groups components of a workspace under a new root. Definition 1.16.1 writes it as ⊔ ∘ (B ⊗ id) ∘ Π_(k) ∘ Δ_P, where the primitive coproduct Δ_P splits a workspace in every way, so FS^(k)(F) sums B(S) ⊔ (F - S) over the k-component subworkspaces S (formSet_of'). On workspaces of syntactic objects it lands in the extended workspaces of (1.16.3) (map_formSet_le).

The book's syntax–semantics interface (Chapter 3) replaces per-feature checking by a single recursive map, the Birkhoff renormalization of a character of the Connes–Kreimer Hopf algebra of the syntactic object. The Boolean parsing semiring Consistency of §3.5 is the target, toCK embeds a syntactic object into the Hopf algebra, featureConsistency is the renormalized character, and headConsistency instantiates it for the head-following character of Lemma 3.2.5, whose probe reads the §1.13 selection head. The machinery is noncomputable, so these are specifications of consistency rather than checkers. In §3.5.2 the operator is the projection of Laurent series onto their polar part. The renormalized part of any character then lands in the power series (truncLT_birkhoffPlus_of'), while the grading character ϕt is already nonpolar and is its own renormalized part (birkhoffPlus_gradingChar), so it cannot single out Sideward Merge.

Obligatory control (§3.8.2) is derived by External Merge alone. In the man tried to read a book both inscriptions of the man merge into theta positions, as repetitions of one another, and Form Copy restricts the object to the diagonal on which they are one (theMan_mem_copyRel), while a book, not structurally identical to the man, is no copy of it (not_mem_copyRel_aBook).

Correspondence with the book

The book's algebra lives in Core/ and in Syntax/Minimalist/{Workspace,Merge,Economy}/:

• Definitions 1.2.6 and 1.2.8 (admissible cuts, the coproducts Δ^ω): ConnesKreimer.cutSummandsN and comulAlgHomN for Δ^ρ, which Remark 1.2.9 identifies with the Connes–Kreimer coproduct; cutSummandsCN and comulCAlgHomN for Δ^c.
• Lemma 1.2.10: ConnesKreimer.comulCN_coassoc and the edge grading of Coproduct/TraceGrading.
• Lemma 1.2.11 and (1.2.12): ConnesKreimer.instBialgebraRho, the HopfAlgebra instance, and antipode_ofTree.
• The projections Π_{ρ,c} and Π_{d,ρ} and the relations Δ^d = (id ⊗ Π_{d,ρ}) ∘ Δ^ρ = (id ⊗ Π_{d,c}) ∘ Δ^c displayed before (1.3.10): ConnesKreimer.eraseTraces, UnorderedTree.contractUnary, ConnesKreimer.cutSummandsDN, ConnesKreimer.comulDAlgHomN, ConnesKreimer.eraseTraces_comulCAlgHomN, contractUnary_eraseTraces_comulCAlgHomN.
• Definition 1.3.4: Minimalist.Merge.mergeOpG over a cut enumeration, with mergeOp at Δ^ρ and mergeOpC at Δ^c; (1.3.11): Minimalist.Merge.mergeOpG_apply_of'.
• Lemma 1.4.1: Minimalist.Merge.mergeOpG_pair, mergeOpG_pair_residual, with the residual workspace passing through by mergeOpG_of'_mul.
• Proposition 1.4.2: Minimalist.Merge.mergeOpG_im_composition; on syntactic objects Minimalist.SyntacticObject.mergeOpC_im, and for a derivation Minimalist.Derivation.mergeOpList_initial.
• Lemmas 1.4.4 and 1.4.5: Minimalist.Merge.mergeOpG_sideward_2b, mergeOpG_sideward_3b, mergeOpG_sideward_3a.
• (1.5.1) and the weights of §1.5.2: Minimalist.Merge.comulEps, mergeOpEps, with comulEps_one and comulEps_zero (the primitive coproduct); Proposition 1.5.1 at ε = 0: mergeOpEps_zero_of'_of_not_le, mergeOpEps_zero_pair_add; at every ε: mergeOpEps_pair, mergeOpEps_im_composition, mergeOpEps_of'_eq_smul_of_not_le.
• Definition 1.6.1 and Proposition 1.6.4: Minimalist.MinimalYield over a counting, MinimalYield.em_pair, em_pair_accessibleCount, im_accessibleCount_of_cut.
• Lemma 1.6.3 (1.6.8) and (1.6.10): ConnesKreimer.cutSummandsCN_accessibleCount, cutSummandsCN_accessibleSize. Proposition 1.6.8 and Remark 1.6.7, on the terms of Merge (Minimalist.Merge.mergeOpG_apply_of'_eq_sum): Minimalist.card_singleton_add_trunk_add_numWhole, accessibleCount_merge_term, accessibleSize_merge_term, MinimalYield.merge_term_accessibleCount_iff, accessibleCount_unit_term for Δ^c, and MinimalYield.merge_term_numEdges_iff for Δ^d.
• Lemma 1.6.3 (1.6.7): ConnesKreimer.cutSummandsDN_numEdges, from the unary vertices a cut leaves (ConnesKreimer.cutSummandsN_numUnary); for Internal Merge, Minimalist.numEdges_im_of_cut, MinimalYieldWeak.im_numEdges_of_cut, MinimalYield.not_im_numEdges_of_cut. Each cut's cost over a workspace: ConnesKreimer.CutChoice.HasExtractionCost.
• Definition 1.6.2 and Proposition 1.6.10: Minimalist.NoComplexityLoss, met by every admissible derivation step (Minimalist.Step.noComplexityLoss); along the induced map of a term of Merge (Minimalist.componentMap, NoComplexityLoss.of_componentMap), NoComplexityLoss.map_componentMap_merge_iff, not_map_componentMap_merge, not_map_componentMap_unit, and at the trace cuts graded by σ, not_map_accessibleSize_componentMap_merge.
• Definition 1.6.2's degree #L: UnorderedTree.numLeaves; Lemma 1.6.3: ConnesKreimer.cutSummandsCN_numNodes.
• The functionals of (1.7.5) and their Lie algebra: Bialgebra.IsDualPrimitive and Bialgebra.dualPrimitives; they are supported on single trees (ConnesKreimer.isDualPrimitive_iff).
• Lemma 1.7.3, for Δ^ρ and grafting at vertices: ConnesKreimer.isDualPrimitive_lcoeff_iff, lie_lcoeff_singleton_apply_ofTree, lie_lcoeff_singleton_apply_of', and GrossmanLarson.pairingLie for the bracket of the grafting product.
• Definition 3.1.1 and the weight +1 identity of Definition 3.1.2: IsRotaBaxter at weights -1 and +1; the identity operator of Remark 3.2.2, at weight +1 on the Boolean semiring: Consistency.isRotaBaxter_id.
• Definitions 3.1.3, 3.1.5 and 3.1.6, Proposition 3.1.7, Remark 3.1.8: ConnesKreimer.birkhoffMinus, birkhoffPrepTree, birkhoffPlus, birkhoffPlus_eq_convMul, birkhoffFactorization, with the operator -R; the subalgebras of Proposition 3.1.7: ConnesKreimer.birkhoffMinus_of'_mem_range, birkhoffPlus_of'_mem_range; Proposition 3.1.9: ConnesKreimer.convMul_birkhoffMinus_apply_ofTree.
• Proposition 3.5.2 and (3.5.4): HahnSeries.isRotaBaxter_truncLT. The gradings of §3.5.2.1: δb₀, δα, δσ, minimalYield_iff_gradings, minimalYieldWeak_iff_truncLT. Proposition 3.5.3 for δα, without the derivation coefficients: gradingChar; Lemma 3.5.5: truncLT_gradingChar_of'; the first step of the proof of Proposition 3.5.6: truncLT_birkhoffPlus_of'.

Implementation notes

In §1.4.4 the book displays the result with the deletion quotient T/d T₂ = {was, eaten}, and alternatively with the contraction quotient T/c T₂, whose contracted leaf it labels by the extracted term {the, apple}. The trace cuts of the carrier label that leaf by the head of the extracted term (traceEncoder), so the example's quotient is {was, {eaten, t}} with t the trace of the.

The equation carries its initial term, X = x t + 𝔐(X, X). The book writes X = 𝔐(X, X) and supplies X₁ = x as an initial condition, but 𝔐(X, X) has no degree-one term (coeff_one_mergeSeries), so the leaf enters as an inhomogeneous term.

TreeAlgebra is spanned by the forests of unlabelled trees, not only by the binary trees of 𝔗. V(𝔗) is the span of the single binary trees in it, and every term of the solution lies there.

formSet is defined for every k on all forests, with the root label of B a parameter. Definition 1.16.1 takes k ≥ 3 and the domain V(𝔉_{SO₀}) of workspaces of syntactic objects; map_formSet_le is stated on that domain, with the bare root label of the syntactic objects.

The proof of Proposition 1.10.2 prints X₄ = 2{x{x{xx}}} + {{xx}{xx}}. Its recursion gives 𝔐(X₁, X₃) + 𝔐(X₂, X₂) + 𝔐(X₃, X₁) = 4{x{x{xx}}} + {{xx}{xx}} (planarSum_four), and four is the number of planar embeddings that the proof says the coefficient counts: the five planar binary trees with four leaves split as four and one.

Definition 3.1.2's weight -1 semiring identity R(a) ⊙ R(b) ⊡ R(a ⊙ b) = R(a ⊙ R(b)) ⊡ R(R(a) ⊙ b) is not the IsRotaBaxter identity at any weight, and Remark 3.2.2 and Lemma 3.2.7 use R = id at that weight on the tropical semiring. On Consistency the identity has weight +1 as well, since disjunction is idempotent, and the consistency maps use it at that weight.

TODO

§1.17 reads (1.10.1) as the quadratic case of the combinatorial Dyson–Schwinger equation X = B(P(X)) of (1.17.2), with the grafting operator B of Definition 1.3.2 and the recursive solution (1.17.3), which the book cites rather than proves. Stating it needs B on formal series in the grading by vertices, in which B raises the degree by one. With x = B(1) the Merge case is P(t) = 1 + t², while the book writes P(X) = X² next to its requirement a₀ = 1.

Lemma 1.10.1 identifies 𝔗 with the free nonassociative commutative magma on one generator; the link to the syntactic-object carrier, the free commutative magma on the lexical items, is not stated.

Lemma 1.16.5 extends the coproducts Δ^ω to extended workspaces by excluding the cuts of edges at a root of valence at least three, so that Merge does not undo the grouping FormSet builds (§1.16.2). It is not formalized.

Proposition 1.6.8's row for the Sideward case 3(a) under Δ^d lowers α by two, counting two contracted edges. When the two terms are sisters, as the and apple are in the apple, the deletion leaves their parent a leaf and contracts nothing, so α is unchanged. The term still diverges, so the proposition's conclusion stands.

Corollary 3.5.4's character ψt sums over the pairs of intermediate derivations of a target, which needs a Merge step relation on workspaces; it, and Proposition 3.5.6 beyond the first step of its proof, are not formalized.

The book's section locators (§1.12.1, §1.13, §1.13.2) are transcribed from an earlier version of this file and are UNVERIFIED against the published text.

References

• [MCB25]
• [CSB+23]

Internal Merge: an example (§1.4.4)

def MarcolliChomskyBerwick2025.tok (c : Minimalist.Cat) (sel : Minimalist.SelStack) (pf : String) (i : ℕ) : Minimalist.LexicalItem.Token

A token of the simple lexical item of category c selecting sel, pronounced pf.

Equations

• MarcolliChomskyBerwick2025.tok c sel pf i = { item := Minimalist.LexicalItem.of c sel pf, id := i }

Sideward Merge, Minimal Search and economy on the workspace of §1.3.4

The workspace {eaten, {the, apple}} of §1.3.4 also admits Sideward Merge of type 2(b), which merges eaten with the cut out of the apple, and the apple alone admits Internal Merge of the and Sideward Merge of type 3(a) of the and apple. On these the general results of §1.4–1.6 give Sideward Merge a nonzero term, which Minimal Search removes at ε = 0 while it keeps External and Internal Merge. The 2(b) term satisfies Minimal Yield under trace counting, as Remark 1.6.9 says. No Complexity Loss excludes it at the pruning cuts graded by vertices, and at the trace cuts graded by the size σ. At the trace cuts the vertex count does not exclude it, because the trace of the takes the place of the.

The core computational structure of Merge (§1.10)

@[reducible, inline]

abbrev MarcolliChomskyBerwick2025.TreeAlgebra : Type

The Connes–Kreimer algebra of unlabelled trees over ℤ, in which the free ℤ-module V(𝔗) on the nonplanar binary trees sits as the span of single trees.

Equations

• MarcolliChomskyBerwick2025.TreeAlgebra = ConnesKreimer ℤ (UnorderedTree Unit)

def MarcolliChomskyBerwick2025.forgetPlanar : BinaryTree Unit → UnorderedTree Unit

Forgetting the planar structure of a planar binary tree, whose leaves are its nils.

Equations

• MarcolliChomskyBerwick2025.forgetPlanar BinaryTree.nil = UnorderedTree.leaf ()
• MarcolliChomskyBerwick2025.forgetPlanar (BinaryTree.node value l r) = UnorderedTree.node () {MarcolliChomskyBerwick2025.forgetPlanar l, MarcolliChomskyBerwick2025.forgetPlanar r}

noncomputable def MarcolliChomskyBerwick2025.generator : TreeAlgebra

The single variable x, the one-leaf tree.

Equations

• MarcolliChomskyBerwick2025.generator = ConnesKreimer.ofTree (UnorderedTree.leaf ())

noncomputable def MarcolliChomskyBerwick2025.mergeLin : TreeAlgebra →ₗ[ℤ] TreeAlgebra →ₗ[ℤ] TreeAlgebra

Merge on V(𝔗) is the grafting operator after the disjoint union (Lemma 1.3.3), a bilinear map.

Equations

• MarcolliChomskyBerwick2025.mergeLin = (LinearMap.mul ℤ MarcolliChomskyBerwick2025.TreeAlgebra).compr₂ (ConnesKreimer.bPlusLin ())

@[simp]

theorem MarcolliChomskyBerwick2025.mergeLin_apply (a b : TreeAlgebra) : (mergeLin a) b = (ConnesKreimer.bPlusLin ()) (a * b)

theorem MarcolliChomskyBerwick2025.mergeLin_comm (a b : TreeAlgebra) : (mergeLin a) b = (mergeLin b) a

theorem MarcolliChomskyBerwick2025.mergeLin_ofTree (s t : UnorderedTree Unit) : (mergeLin (ConnesKreimer.ofTree s)) (ConnesKreimer.ofTree t) = ConnesKreimer.ofTree (UnorderedTree.node () {s, t})

noncomputable def MarcolliChomskyBerwick2025.mergeSeries (X Y : PowerSeries TreeAlgebra) : PowerSeries TreeAlgebra

Merge extends to formal series X = ∑ Xₗ degree by degree, the degree-n term of 𝔐(X, Y) being ∑_{i+j=n} 𝔐(Xᵢ, Yⱼ).

Equations

• MarcolliChomskyBerwick2025.mergeSeries X Y = PowerSeries.mk fun (n : ℕ) => (ConnesKreimer.bPlusLin ()) ((PowerSeries.coeff n) (X * Y))

@[simp]

theorem MarcolliChomskyBerwick2025.coeff_mergeSeries (X Y : PowerSeries TreeAlgebra) (n : ℕ) : (PowerSeries.coeff n) (mergeSeries X Y) = ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, (mergeLin ((PowerSeries.coeff p.1) X)) ((PowerSeries.coeff p.2) Y)

theorem MarcolliChomskyBerwick2025.coeff_one_mergeSeries {X : PowerSeries TreeAlgebra} (h0 : (PowerSeries.coeff 0) X = 0) : (PowerSeries.coeff 1) (mergeSeries X X) = 0

𝔐(X, X) has no degree-one term, so the printed X = 𝔐(X, X) cannot meet X₁ = x.

def MarcolliChomskyBerwick2025.IsMergeSolution (X : PowerSeries TreeAlgebra) : Prop

A series solves (1.10.1) with its initial condition X₁ = x when it has no constant term and X = x t + 𝔐(X, X).

Equations

• MarcolliChomskyBerwick2025.IsMergeSolution X = ((PowerSeries.coeff 0) X = 0 ∧ X = (PowerSeries.monomial 1) MarcolliChomskyBerwick2025.generator + MarcolliChomskyBerwick2025.mergeSeries X X)

noncomputable def MarcolliChomskyBerwick2025.planarSum : ℕ → TreeAlgebra

The formal sum of the planar binary trees with n leaves, planarity forgotten.

Equations

• MarcolliChomskyBerwick2025.planarSum 0 = 0
• MarcolliChomskyBerwick2025.planarSum n.succ = ∑ P ∈ BinaryTree.treesOfNumNodesEq n, ConnesKreimer.ofTree (MarcolliChomskyBerwick2025.forgetPlanar P)

noncomputable def MarcolliChomskyBerwick2025.mergeSolution : PowerSeries TreeAlgebra

The series X = ∑ₗ Xₗ of Proposition 1.10.2.

Equations

• MarcolliChomskyBerwick2025.mergeSolution = PowerSeries.mk MarcolliChomskyBerwick2025.planarSum

theorem MarcolliChomskyBerwick2025.planarSum_add_two (n : ℕ) : planarSum (n + 2) = ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, (mergeLin (planarSum (p.1 + 1))) (planarSum (p.2 + 1))

The recursion of the proof of Proposition 1.10.2, Xₙ = ∑_{j=1}^{n-1} 𝔐(Xⱼ, X_{n-j}).

theorem MarcolliChomskyBerwick2025.isMergeSolution_mergeSolution : IsMergeSolution mergeSolution

The sum of the planar binary trees solves (1.10.1) with X₁ = x (Proposition 1.10.2).

theorem MarcolliChomskyBerwick2025.IsMergeSolution.eq {X : PowerSeries TreeAlgebra} (h : IsMergeSolution X) : X = mergeSolution

The solution of Proposition 1.10.2 is unique, since the recursion determines each term from the lower ones.

theorem MarcolliChomskyBerwick2025.coeff_planarSum_succ (n : ℕ) (T : UnorderedTree Unit) : ConnesKreimer.coeff (planarSum (n + 1)) {T} = ↑{P ∈ BinaryTree.treesOfNumNodesEq n | forgetPlanar P = T}.card

The coefficient of a nonplanar tree in Xₙ₊₁ is its number of planar embeddings.

theorem MarcolliChomskyBerwick2025.aeval_planarSum_succ (n : ℕ) : (ConnesKreimer.aeval fun (x : UnorderedTree Unit) => 1) (planarSum (n + 1)) = ↑(catalan n)

The coefficients of Xₙ₊₁ sum to the Catalan number Cₙ, the number of planar binary trees with n + 1 leaves.

theorem MarcolliChomskyBerwick2025.planarSum_one : planarSum 1 = generator

X₁ = x.

theorem MarcolliChomskyBerwick2025.planarSum_two : planarSum 2 = (mergeLin generator) generator

X₂ = {xx}.

theorem MarcolliChomskyBerwick2025.planarSum_three : planarSum 3 = 2 • (mergeLin generator) ((mergeLin generator) generator)

X₃ = {x{xx}} + {{xx}x} = 2{x{xx}}.

theorem MarcolliChomskyBerwick2025.planarSum_four : planarSum 4 = 4 • (mergeLin generator) ((mergeLin generator) ((mergeLin generator) generator)) + (mergeLin ((mergeLin generator) generator)) ((mergeLin generator) generator)

X₄ = 4{x{x{xx}}} + {{xx}{xx}}; the proof of Proposition 1.10.2 prints the coefficient 2.

Externalization (§1.12–1.13)

FormSet (§1.16)

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

FormSet FS^(k) = ⊔ ∘ (B ⊗ id) ∘ Π_(k) ∘ Δ_P (Definition 1.16.1, (1.16.2)) splits the workspace by the primitive coproduct, keeps the terms whose left factor has k components, grafts those under a new root labelled a, and multiplies back.

Equations

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

theorem MarcolliChomskyBerwick2025.formSet_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (a : α) (k : ℕ) (F : UnorderedTree.Forest (UnorderedTree α)) : (formSet a k) (ConnesKreimer.of' F) = (Multiset.map (fun (S : Multiset (UnorderedTree α)) => ConnesKreimer.of' (UnorderedTree.node a S ::ₘ (F - S))) (Multiset.powersetCard k F)).sum

FormSet groups k components of a workspace in every way, summing B(S) ⊔ (F - S) over the k-component subworkspaces S of F, counted with multiplicity (Remark 1.16.4).

theorem MarcolliChomskyBerwick2025.formSet_of'_of_card_lt {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (a : α) {k : ℕ} {F : UnorderedTree.Forest (UnorderedTree α)} (h : Multiset.card F < k) : (formSet a k) (ConnesKreimer.of' F) = 0

With fewer than k components there is nothing to group.

theorem MarcolliChomskyBerwick2025.formSet_of'_card {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (a : α) (F : UnorderedTree.Forest (UnorderedTree α)) : (formSet a (Multiset.card F)) (ConnesKreimer.of' F) = ConnesKreimer.ofTree (UnorderedTree.node a F)

With exactly k components FormSet groups the whole workspace, as in the unbounded unstructured sequences of p. 144.

def MarcolliChomskyBerwick2025.IsExtendedWorkspace (G : UnorderedTree.Forest (UnorderedTree Minimalist.SyntacticObject.Vertex)) : Prop

A forest is an extended workspace, in 𝔉̃ᴿ of (1.16.3), when each component is a syntactic object or a bare root of any valence over syntactic objects, binary below that root.

Equations

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

theorem MarcolliChomskyBerwick2025.map_formSet_le {R : Type u_1} [CommSemiring R] (k : ℕ) : Submodule.map (formSet Minimalist.SyntacticObject.Vertex.bare k) (Submodule.span R (ConnesKreimer.of' '' {F : UnorderedTree.Forest (UnorderedTree Minimalist.SyntacticObject.Vertex) | ∀ T ∈ F, Minimalist.IsSyntacticObject T})) ≤ Submodule.span R (ConnesKreimer.of' '' {G : UnorderedTree.Forest (UnorderedTree Minimalist.SyntacticObject.Vertex) | IsExtendedWorkspace G})

On workspaces of syntactic objects, the range of FormSet lies in the span of the extended workspaces (Definition 1.16.1).

Feature consistency as Birkhoff renormalization (Chapter 3)

inductive MarcolliChomskyBerwick2025.Consistency : Type

The Boolean consistency semiring of §3.5, the two-element idempotent commutative semiring with disjunction as addition, some decomposition being consistent, and conjunction as multiplication, all parts agreeing.

• inconsistent : Consistency
• consistent : Consistency

@[instance_reducible]

instance MarcolliChomskyBerwick2025.instDecidableEqConsistency : DecidableEq Consistency

Equations

• MarcolliChomskyBerwick2025.instDecidableEqConsistency x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MarcolliChomskyBerwick2025.instReprConsistency.repr : Consistency → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance MarcolliChomskyBerwick2025.instReprConsistency : Repr Consistency

Equations

• MarcolliChomskyBerwick2025.instReprConsistency = { reprPrec := MarcolliChomskyBerwick2025.instReprConsistency.repr }

@[instance_reducible]

instance MarcolliChomskyBerwick2025.instInhabitedConsistency : Inhabited Consistency

Equations

• MarcolliChomskyBerwick2025.instInhabitedConsistency = { default := MarcolliChomskyBerwick2025.instInhabitedConsistency.default }

@[instance_reducible]

instance MarcolliChomskyBerwick2025.instFintypeConsistency : Fintype Consistency

Equations

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

def MarcolliChomskyBerwick2025.Consistency.or : Consistency → Consistency → Consistency

Disjunction, consistent iff at least one argument is.

Equations

• MarcolliChomskyBerwick2025.Consistency.consistent.or x✝ = MarcolliChomskyBerwick2025.Consistency.consistent
• x✝.or MarcolliChomskyBerwick2025.Consistency.consistent = MarcolliChomskyBerwick2025.Consistency.consistent
• x✝¹.or x✝ = MarcolliChomskyBerwick2025.Consistency.inconsistent

def MarcolliChomskyBerwick2025.Consistency.and : Consistency → Consistency → Consistency

Conjunction, consistent iff both arguments are.

Equations

• MarcolliChomskyBerwick2025.Consistency.consistent.and MarcolliChomskyBerwick2025.Consistency.consistent = MarcolliChomskyBerwick2025.Consistency.consistent
• x✝¹.and x✝ = MarcolliChomskyBerwick2025.Consistency.inconsistent

@[instance_reducible]

instance MarcolliChomskyBerwick2025.Consistency.instCommSemiring : CommSemiring Consistency

Equations

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

theorem MarcolliChomskyBerwick2025.Consistency.isRotaBaxter_id : IsRotaBaxter 1 id

The identity is a Rota–Baxter operator of weight +1 on Consistency, since disjunction is idempotent and absorbs the weight term. On a Boolean target the threshold operator collapses to the identity, disagreement already being the additive zero.

noncomputable def MarcolliChomskyBerwick2025.toCK (S : Minimalist.SyntacticObject) : ConnesKreimer ℕ (UnorderedTree Minimalist.SyntacticObject.Vertex)

A syntactic object as an element of the Connes–Kreimer Hopf algebra over ℕ, the singleton forest of its underlying nonplanar tree. The base ring is ℕ because every commutative semiring, Consistency included, is an ℕ-algebra, while a Boolean target is no ℤ-algebra.

Equations

• MarcolliChomskyBerwick2025.toCK S = ConnesKreimer.ofTree ↑S

theorem MarcolliChomskyBerwick2025.toCK_merge (l r : Minimalist.SyntacticObject) : toCK (l.merge r) = (ConnesKreimer.bPlusLin Minimalist.SyntacticObject.Vertex.bare) (toCK l * toCK r)

Merge factors through the grafting operator on the disjoint union of its arguments, with the bare root label (Lemma 1.3.3).

noncomputable def MarcolliChomskyBerwick2025.featureConsistency (φ : ConnesKreimer ℕ (UnorderedTree Minimalist.SyntacticObject.Vertex) →ₗ[ℕ] Consistency) (P : Consistency →+ Consistency) (S : Minimalist.SyntacticObject) : Consistency

The feature-consistency map φ₊ on a syntactic object, the value at the object of the renormalized part of a feature character φ under an operator P on Consistency. It is the single recursive map of §3.1.5 that checks consistency over all substructures.

Equations

• MarcolliChomskyBerwick2025.featureConsistency φ P S = ConnesKreimer.birkhoffPlusTree φ P ↑S

theorem MarcolliChomskyBerwick2025.featureConsistency_eq_convMul (φ : ConnesKreimer ℕ (UnorderedTree Minimalist.SyntacticObject.Vertex) →ₗ[ℕ] Consistency) (P : Consistency →+ Consistency) (hφ : φ 1 = 1) (S : Minimalist.SyntacticObject) : (WithConv.toConv (ConnesKreimer.birkhoffMinus φ P).toLinearMap * WithConv.toConv φ).ofConv (toCK S) = featureConsistency φ P S

The feature-consistency map factors as the semiring Birkhoff convolution φ₊ = φ₋ ⋆ φ on the object's Hopf-algebra image (Definition 3.1.6, Proposition 3.1.9), for a unital φ.

def MarcolliChomskyBerwick2025.headProbeTree (Υ : Minimalist.LexicalItem.Token → Consistency) (T : UnorderedTree Minimalist.SyntacticObject.Vertex) : Consistency

The head-probe value Υ_{s,h} on a tree (equation (3.2.1)), the probe Υ applied to the tree's selection head, and inconsistent when the tree has no well-defined head.

Equations

• MarcolliChomskyBerwick2025.headProbeTree Υ T = (Minimalist.selCheckN T).head.elim MarcolliChomskyBerwick2025.Consistency.inconsistent Υ

noncomputable def MarcolliChomskyBerwick2025.headProbeChar (Υ : Minimalist.LexicalItem.Token → Consistency) : ConnesKreimer ℕ (UnorderedTree Minimalist.SyntacticObject.Vertex) →ₐ[ℕ] Consistency

The head-following feature character ϕ_{Υ,s,h} of Lemma 3.2.5 is the algebra homomorphism extending Υ_{s,h} multiplicatively to forests, so that a workspace is consistent iff each of its trees is. It is the unrenormalized feature assignment whose Birkhoff renormalization is the consistency map.

Equations

• MarcolliChomskyBerwick2025.headProbeChar Υ = ConnesKreimer.aeval (MarcolliChomskyBerwick2025.headProbeTree Υ)

@[simp]

theorem MarcolliChomskyBerwick2025.headProbeChar_apply_of' (Υ : Minimalist.LexicalItem.Token → Consistency) (F : UnorderedTree.Forest (UnorderedTree Minimalist.SyntacticObject.Vertex)) : (headProbeChar Υ) (ConnesKreimer.of' F) = (Multiset.map (headProbeTree Υ) F).prod

@[simp]

theorem MarcolliChomskyBerwick2025.headProbeChar_apply_ofTree (Υ : Minimalist.LexicalItem.Token → Consistency) (T : UnorderedTree Minimalist.SyntacticObject.Vertex) : (headProbeChar Υ) (ConnesKreimer.ofTree T) = headProbeTree Υ T

theorem MarcolliChomskyBerwick2025.headProbeChar_one (Υ : Minimalist.LexicalItem.Token → Consistency) : (headProbeChar Υ) 1 = 1

noncomputable def MarcolliChomskyBerwick2025.headConsistency (Υ : Minimalist.LexicalItem.Token → Consistency) (S : Minimalist.SyntacticObject) : Consistency

The feature-consistency verdict on a syntactic object (§3.1.5, Lemmas 3.2.5 and 3.2.7), the Birkhoff renormalization with the identity operator of the head-following character, consistent iff the head-probe agreements cohere across all substructures.

Equations

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

theorem MarcolliChomskyBerwick2025.headConsistency_eq_convMul (Υ : Minimalist.LexicalItem.Token → Consistency) (S : Minimalist.SyntacticObject) : (WithConv.toConv (ConnesKreimer.birkhoffMinus (headProbeChar Υ).toLinearMap (AddMonoidHom.id Consistency)).toLinearMap * WithConv.toConv (headProbeChar Υ).toLinearMap).ofConv (toCK S) = headConsistency Υ S

The head-driven verdict factors as the semiring Birkhoff convolution φ₊ = φ₋ ⋆ φ of the head-following character (Definition 3.1.6, Lemma 3.2.7).

Minimal Yield and the polar part of Laurent series (§3.5.2)

def MarcolliChomskyBerwick2025.δb₀ {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : ℤ

δb₀ F F' = b₀ F − b₀ F', nonnegative iff F → F' does not diverge.

Equations

• MarcolliChomskyBerwick2025.δb₀ F F' = ↑(Multiset.card F) - ↑(Multiset.card F')

def MarcolliChomskyBerwick2025.δα {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : ℤ

δα F F' = α F' − α F, nonnegative iff F → F' loses no information.

Equations

• MarcolliChomskyBerwick2025.δα F F' = ↑(Multiset.map UnorderedTree.numEdges F').sum - ↑(Multiset.map UnorderedTree.numEdges F).sum

def MarcolliChomskyBerwick2025.δσ {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : ℤ

δσ F F' = σ F' − σ F, equal to 1 iff F → F' has minimal yield.

Equations

• MarcolliChomskyBerwick2025.δσ F F' = ↑(Multiset.map UnorderedTree.numNodes F').sum - ↑(Multiset.map UnorderedTree.numNodes F).sum

theorem MarcolliChomskyBerwick2025.δσ_eq {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : δσ F F' = δα F F' - δb₀ F F'

theorem MarcolliChomskyBerwick2025.minimalYieldWeak_iff_gradings {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : Minimalist.MinimalYieldWeak UnorderedTree.numEdges F F' ↔ 0 ≤ δb₀ F F' ∧ 0 ≤ δα F F'

theorem MarcolliChomskyBerwick2025.minimalYield_iff_gradings {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : Minimalist.MinimalYield UnorderedTree.numEdges F F' ↔ 0 ≤ δb₀ F F' ∧ 0 ≤ δα F F' ∧ δσ F F' = 1

theorem MarcolliChomskyBerwick2025.minimalYieldWeak_iff_truncLT {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommRing R] (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) [Nontrivial R] : Minimalist.MinimalYieldWeak UnorderedTree.numEdges F F' ↔ (HahnSeries.truncLT 0) ((HahnSeries.single (δb₀ F F')) 1) = 0 ∧ (HahnSeries.truncLT 0) ((HahnSeries.single (δα F F')) 1) = 0

Weak Minimal Yield holds iff the δb₀- and δα-monomials of F → F' are both nonpolar.

noncomputable def MarcolliChomskyBerwick2025.gradingChar {α : Type u_1} {R : Type u_3} [CommRing R] : ConnesKreimer R (UnorderedTree α) →ₐ[R] LaurentSeries R

The character ϕt of Proposition 3.5.3 for δ = δα, recording only the grading, sends a tree T to t^{α(T)}, multiplicatively over disjoint union.

Equations

• MarcolliChomskyBerwick2025.gradingChar = ConnesKreimer.aeval fun (T : UnorderedTree α) => (HahnSeries.single ↑T.numEdges) 1

theorem MarcolliChomskyBerwick2025.gradingChar_apply_of' {α : Type u_1} {R : Type u_3} [CommRing R] (F : UnorderedTree.Forest (UnorderedTree α)) : gradingChar (ConnesKreimer.of' F) = (HahnSeries.single ↑(Multiset.map UnorderedTree.numEdges F).sum) 1

ϕt(F) = t^{α(F)}, since α is additive over forests.

theorem MarcolliChomskyBerwick2025.truncLT_gradingChar_of' {α : Type u_1} {R : Type u_3} [CommRing R] (F : UnorderedTree.Forest (UnorderedTree α)) : (HahnSeries.truncLT 0) (gradingChar (ConnesKreimer.of' F)) = 0

ϕt is nonpolar on every forest, since α(F) ≥ 0 (Lemma 3.5.5).

theorem MarcolliChomskyBerwick2025.birkhoffPlus_gradingChar {α : Type u_1} {R : Type u_3} [CommRing R] : ConnesKreimer.birkhoffPlus gradingChar.toLinearMap (-(HahnSeries.truncLTLinearMap R 0).toAddMonoidHom) = gradingChar

ϕt is its own renormalized part. Being nonpolar, it has no negative part, so the Birkhoff factorization removes nothing and cannot separate Sideward Merge from Internal and External Merge.

theorem MarcolliChomskyBerwick2025.truncLT_single_mul_ne {R : Type u_3} [CommRing R] [Nontrivial R] : (HahnSeries.truncLT 0) ((HahnSeries.single (-2)) 1 * (HahnSeries.single 1) 1) ≠ (HahnSeries.truncLT 0) ((HahnSeries.single (-2)) 1) * (HahnSeries.truncLT 0) ((HahnSeries.single 1) 1)

The polar projection is not multiplicative: t⁻² · t = t⁻¹ is polar while t is not, so a product can acquire a polar part that its factors lack. Hence (1 − R) ∘ φ need not be a character, and renormalization goes through the Birkhoff factorization.

theorem MarcolliChomskyBerwick2025.truncLT_birkhoffMinus_of' {α : Type u_1} {R : Type u_3} [CommRing R] (φ : ConnesKreimer R (UnorderedTree α) →ₐ[R] LaurentSeries R) {F : UnorderedTree.Forest (UnorderedTree α)} (hF : F ≠ 0) : (HahnSeries.truncLT 0) ((ConnesKreimer.birkhoffMinus φ.toLinearMap (-(HahnSeries.truncLTLinearMap R 0).toAddMonoidHom)) (ConnesKreimer.of' F)) = (ConnesKreimer.birkhoffMinus φ.toLinearMap (-(HahnSeries.truncLTLinearMap R 0).toAddMonoidHom)) (ConnesKreimer.of' F)

The negative part of every character into Laurent series is polar on nonempty forests, landing in the subalgebra R(A[t⁻¹][[t]]) of Proposition 3.1.7.

theorem MarcolliChomskyBerwick2025.truncLT_birkhoffPlus_of' {α : Type u_1} {R : Type u_3} [CommRing R] (φ : ConnesKreimer R (UnorderedTree α) →ₐ[R] LaurentSeries R) (F : UnorderedTree.Forest (UnorderedTree α)) : (HahnSeries.truncLT 0) ((ConnesKreimer.birkhoffPlus φ.toLinearMap (-(HahnSeries.truncLTLinearMap R 0).toAddMonoidHom)) (ConnesKreimer.of' F)) = 0

The renormalized part of every character into Laurent series is nonpolar, landing in the subalgebra (1 − R)(A[t⁻¹][[t]]) = A[[t]] of Proposition 3.1.7: the first step of the proof of Proposition 3.5.6.

Obligatory control by Form Copy (§3.8.2)

noncomputable def MarcolliChomskyBerwick2025.theMan : Minimalist.SyntacticObject

The controller the man, from tokens 0 and 1.

Equations

• MarcolliChomskyBerwick2025.theMan = (↑(MarcolliChomskyBerwick2025.tok Minimalist.Cat.D [Minimalist.Cat.N] "the" 0)).merge ↑(MarcolliChomskyBerwick2025.tok Minimalist.Cat.N [] "man" 1)

noncomputable def MarcolliChomskyBerwick2025.theMan' : Minimalist.SyntacticObject

The controlled subject the man, from fresh tokens 4 and 5.

Equations

• MarcolliChomskyBerwick2025.theMan' = (↑(MarcolliChomskyBerwick2025.tok Minimalist.Cat.D [Minimalist.Cat.N] "the" 4)).merge ↑(MarcolliChomskyBerwick2025.tok Minimalist.Cat.N [] "man" 5)

noncomputable def MarcolliChomskyBerwick2025.aBook : Minimalist.SyntacticObject

a book, the object of read.

Equations

• MarcolliChomskyBerwick2025.aBook = (↑(MarcolliChomskyBerwick2025.tok Minimalist.Cat.D [Minimalist.Cat.N] "a" 7)).merge ↑(MarcolliChomskyBerwick2025.tok Minimalist.Cat.N [] "book" 8)

noncomputable def MarcolliChomskyBerwick2025.triedToRead : Minimalist.SyntacticObject

The syntactic object (3.8.4) of the man tried to read a book is built by External Merge alone. The controller merges into the theta position of tried and the controlled subject into that of read, since Internal Merge into a theta position would break the dichotomy of §3.8.1.

Equations

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

theorem MarcolliChomskyBerwick2025.theMan_isRepetition : theMan.IsRepetition theMan'

The two inscriptions of the man are repetitions, structurally identical distinct tokens.

theorem MarcolliChomskyBerwick2025.theMan_mem_copyRel : (theMan, theMan') ∈ triedToRead.copyRel

Form Copy relates the controller to the controlled subject, the restriction of (3.8.4) to the diagonal Diag₁,₄ of (3.8.5).

theorem MarcolliChomskyBerwick2025.not_mem_copyRel_aBook : (theMan, aBook) ∉ triedToRead.copyRel

a book is no copy of the man, since Form Copy relates only structurally identical inscriptions.