Docs / Syntax / Minimalist / Workspace / MinimalYield

Minimal Yield

import Linglib.Syntax.Minimalist.Workspace.MinimalYield · namespace Minimalist

Source

Minimal Yield (Definition 1.6.1 of Marcolli, Chomsky and Berwick) is a condition on a transformation F → F' of workspaces. The number b₀ of components does not grow (no divergence), the number α of accessible terms does not fall (no information loss), and the size σ = b₀ + α grows by exactly one (minimality of yield). MinimalYieldWeak is the first two bounds and MinimalYield all three. Both take the count of accessible terms of a component as a parameter, since Proposition 1.6.4 evaluates the one condition under two countings: the deletion coproduct counts every non-root vertex (UnorderedTree.numEdges), the trace coproduct every non-root vertex but its trace leaves (UnorderedTree.accessibleCount).

A term of Merge chooses a cut for each component of the workspace. Each component it takes whole lowers b₀ by one, and each tree it extracts costs a fixed number k of accessible terms (CutChoice.HasExtractionCost): one under the trace coproduct, and two under the deletion coproduct on full binary trees (Lemma 1.6.3). When extractions cost one, a term satisfies Minimal Yield exactly when it takes an object whole, so External Merge and the Sideward case 2(b) pass and the cases 3(a) and 3(b) fail (Proposition 1.6.8). When they cost two, only External Merge passes, and 2(b) satisfies only the weak form. Internal Merge gains one accessible term under the trace coproduct and none under the deletion coproduct, where it satisfies only the weak form (Proposition 1.6.4).

Main definitions

Main results

References

The Minimal Yield principle

The weak Minimal Yield principle, for the count acc of the accessible terms of a component, allows no increase in the number b₀ of components and no decrease in the number α of accessible terms.

structure MinimalYieldWeakL65–70
{κ : Type u_3} (acc : κ → ℕ) (F F' : Multiset κ) :
Prop
  • noDivergence : F'.card ≤ F.card
  • noInfoLoss : (Multiset.map acc F).sum ≤ (Multiset.map acc F').sum

Used by MinimalYield, minimalYieldWeak_iff_signature_le, MinimalYieldWeak.numWhole_ne_zero, MinimalYieldWeak.merge_term_iff_of_extraction_two, MinimalYieldWeak.not_of_forall_notMem, MinimalYieldWeak.im_numEdges_of_cut, MinimalYieldWeak.merge_term_numEdges_iff

Used in MarcolliChomskyBerwick2025

The Minimal Yield principle is the weak form together with the size σ = b₀ + α going up by exactly one.

structure MinimalYieldL72–76
{κ : Type u_3} (acc : κ → ℕ) (F F' : Multiset κ) extends MinimalYieldWeak acc F F' :
Prop
  • noDivergence : F'.card ≤ F.card
  • noInfoLoss : (Multiset.map acc F).sum ≤ (Multiset.map acc F').sum
  • minimalYield : F'.card + (Multiset.map acc F').sum = F.card + (Multiset.map acc F).sum + 1

Built from

Used by MinimalYield.add_right, MinimalYield.merge_term_iff_of_extraction_one, MinimalYield.merge_term_iff_of_extraction_two, MinimalYield.not_of_forall_notMem, MinimalYield.em_pair, MinimalYield.em_pair_accessibleCount, MinimalYield.not_im_numEdges_of_cut, MinimalYield.im_accessibleCount_of_cut, MinimalYield.merge_term_numEdges_iff, MinimalYield.merge_term_accessibleCount_iff

Used in Syntax/Minimalist/Workspace/Derivation, KitaharaSeely2026, MarcolliChomskyBerwick2025

L78–86

MinimalYieldWeak as a Pareto pullback preorder

Terms of Merge and of its unit stage

A term of Merge or of its unit stage on F chooses a cut for each component of F (mergeOpG_apply_of'_eq_sum, mergeOpUnitG_apply_of'_eq_sum). Its workspace holds the object X built from the crown beside the trunk.

L110–116
L118–124
L126–137

When each extraction costs one accessible term, as under Δ^c, a Merge term satisfies Minimal Yield iff some merged object is an unextracted workspace component (Lemma 1.6.3 (1.6.8)).

theorem MinimalYield.merge_term_iff_of_extraction_oneL139–147
{α : Type u_1} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} {F : UnorderedTree.Forest (UnorderedTree α)} {s : ConnesKreimer.CutChoice α} {acc : UnorderedTree α → ℕ} (hs : s ∈ ConnesKreimer.forestCutChoicesG cuts F) (hc : ConnesKreimer.CutChoice.HasExtractionCost acc 1 s) {S S' X : UnorderedTree α} (hK : s.crown = {S, S'}) (hX : acc X = acc S + acc S' + 2) :
MinimalYield acc F ({X} + s.trunk) ↔ s.numWhole ≠ 0

Built from

When each extraction costs two accessible terms, as under Δ^d, a Merge term satisfies Minimal Yield iff both merged objects are unextracted workspace components (Lemma 1.6.3 (1.6.7)).

theorem MinimalYield.merge_term_iff_of_extraction_twoL149–159
{α : Type u_1} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} {F : UnorderedTree.Forest (UnorderedTree α)} {s : ConnesKreimer.CutChoice α} {acc : UnorderedTree α → ℕ} (hs : s ∈ ConnesKreimer.forestCutChoicesG cuts F) (hc : ConnesKreimer.CutChoice.HasExtractionCost acc 2 s) {S S' X : UnorderedTree α} (hK : s.crown = {S, S'}) (hX : acc X = acc S + acc S' + 2) :
MinimalYield acc F ({X} + s.trunk) ↔ s.numWhole = 2

Built from

L161–169
L171–181

A term whose crown contains no workspace component violates Minimal Yield under any counting (Marcolli et al. 2025 Proposition 1.6.8, Remark 1.6.7).

theorem MinimalYieldWeak.not_of_forall_notMemL183–189
{α : Type u_1} [DecidableEq (UnorderedTree α)] {cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)} {F : UnorderedTree.Forest (UnorderedTree α)} {s : ConnesKreimer.CutChoice α} (acc : UnorderedTree α → ℕ) (hs : s ∈ ConnesKreimer.forestCutChoicesG cuts F) (hK : ∀ T ∈ s.crown, T ∉ F) (X : UnorderedTree α) :
¬MinimalYieldWeak acc F ({X} + s.trunk)

Built from

L191–195

External Merge

External Merge is the term of Merge that takes both of its objects whole. It extracts nothing, so it satisfies Minimal Yield whatever extractions cost.

Internal Merge

Internal Merge extracts a term v of T and merges it with what remains.

L236–240

Internal Merge through a deletion cut of a full binary tree satisfies the weak form of Minimal Yield under deletion counting.

theorem MinimalYieldWeak.im_numEdges_of_cutL242–248
{α : Type u_1} {β : Type u_2} (lbl : α) {T : UnorderedTree (α ⊕ β)} {p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)} {v : UnorderedTree (α ⊕ β)} (hT : T.IsFullBinary) (hp : p ∈ ConnesKreimer.cutSummandsDN T) (hv : p.1 = {v}) :
MinimalYieldWeak UnorderedTree.numEdges {T} {UnorderedTree.node (Sum.inl lbl) {v, p.2}}

Built from

Internal Merge through a deletion cut of a full binary tree violates Minimal Yield under deletion counting, since its size σ does not grow.

theorem MinimalYield.not_im_numEdges_of_cutL250–259
{α : Type u_1} {β : Type u_2} (lbl : α) {T : UnorderedTree (α ⊕ β)} {p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)} {v : UnorderedTree (α ⊕ β)} (hT : T.IsFullBinary) (hp : p ∈ ConnesKreimer.cutSummandsDN T) (hv : p.1 = {v}) :
¬MinimalYield UnorderedTree.numEdges {T} {UnorderedTree.node (Sum.inl lbl) {v, p.2}}

Built from

L263–279

Internal Merge through a trace cut satisfies Minimal Yield under trace counting, with Δb₀ = 0, Δα = +1 and Δσ = +1.

theorem MinimalYield.im_accessibleCount_of_cutL281–294
{α : Type u_1} {β : Type u_2} (lbl a₀ : α) (τ : UnorderedTree (α ⊕ β) → β) (F₀ : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) (p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) (hp : p ∈ ConnesKreimer.cutSummandsCN τ (UnorderedTree.node (Sum.inl a₀) F₀)) (v : UnorderedTree (α ⊕ β)) (hv : p.1 = {v}) :
MinimalYield UnorderedTree.accessibleCount {UnorderedTree.node (Sum.inl a₀) F₀} {UnorderedTree.node (Sum.inl lbl) {v, p.2}}

Built from

Terms of Merge under deletion counting

On a full binary workspace, a term of Merge that takes an object whole extracts at most one tree from each component, which costs two accessible terms (1.6.7). A term that takes neither object whole diverges, whatever its extractions cost.

Under deletion counting, on a full binary workspace, a term of Merge satisfies Minimal Yield exactly when it takes both of its objects whole (Marcolli et al. 2025 Propositions 1.6.4 and 1.6.8, for Δ^d).

theorem MinimalYield.merge_term_numEdges_iffL316–326
{α : Type u_1} [DecidableEq (UnorderedTree α)] {F : UnorderedTree.Forest (UnorderedTree α)} {s : ConnesKreimer.CutChoice α} {S S' X : UnorderedTree α} (hF : ∀ T ∈ F, T.IsFullBinary) (hs : s ∈ ConnesKreimer.forestCutChoicesG ConnesKreimer.cutSummandsDN F) (hK : s.crown = {S, S'}) (hX : X.numEdges = S.numEdges + S'.numEdges + 2) :
MinimalYield UnorderedTree.numEdges F ({X} + s.trunk) ↔ s.numWhole = 2

Built from

L328–335

Terms of Merge under trace counting

L346–356
L358–367

Under trace counting, a Merge term satisfies Minimal Yield iff some merged object is an unextracted workspace component (Marcolli et al. 2025 Proposition 1.6.8).

theorem MinimalYield.merge_term_accessibleCount_iffL369–379
{α : Type u_1} {β : Type u_2} [DecidableEq (UnorderedTree (α ⊕ β))] {τ : UnorderedTree (α ⊕ β) → β} {F : UnorderedTree.Forest (UnorderedTree (α ⊕ β))} {s : ConnesKreimer.CutChoice (α ⊕ β)} (a : α) (hs : s ∈ ConnesKreimer.forestCutChoicesG (ConnesKreimer.cutSummandsCN τ) F) (hF : ∀ x ∈ s, x.2.1 ≠ 0 → x.1.value.isLeft = true) {S S' : UnorderedTree (α ⊕ β)} (hK : s.crown = {S, S'}) :
MinimalYield UnorderedTree.accessibleCount F ({UnorderedTree.node (Sum.inl a) {S, S'}} + s.trunk) ↔ s.numWhole ≠ 0

Built from

L381–391