Minimal Yield

Minimal Yield is a condition on a transformation F → F' of workspaces, stated on the size measures of a workspace, its components Multiset.card, its accessible terms Forest.numEdges, and its vertices Forest.numNodes: the number of components does not grow (no divergence), the number of accessible terms does not fall (no information loss), and the number of vertices grows by exactly one (minimality of yield). MinimalYieldWeak is the first two bounds and MinimalYield all three. The weak form is monotonicity of the signature (b₀ᵒᵈ, α), so it is a pullback preorder on workspaces (MinimalYieldWeak.pullbackPreorder). The trace-aware measures are those of Workspace/TraceMeasures.lean.

The per-case theorems evaluate the condition on the shapes the cases of Merge produce, on the carrier UnorderedTree (α ⊕ β) with Sum.inl lexical and Sum.inr trace: External Merge satisfies it; Internal Merge preserves all three measures under Δᵈ counting and raises the trace-aware count and size by one under Δᶜ counting, given the accessible-term extraction identities; the divergent Sideward cases 3(a) and 3(b), which raise the number of components, violate both forms.

Main definitions

• Minimalist.MinimalYieldWeak, Minimalist.MinimalYield
• Minimalist.MinimalYield.signature: the Pareto signature (b₀ᵒᵈ, α).

Main results

• Minimalist.MinimalYield.em_pair: External Merge satisfies Minimal Yield.
• Minimalist.MinimalYield.not_sideward_3a, not_sideward_3b: the divergent Sideward cases do not.

References

• [marcolli-chomsky-berwick-2025], §1.6.1–1.6.2 (Definition 1.6.1, Lemma 1.6.3, Propositions 1.6.4 and 1.6.8)

The Minimal Yield principle

structure Minimalist.MinimalYieldWeak {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : Prop

The weak Minimal Yield principle: no increase in b₀, no decrease in α.

• noDivergence : Multiset.card F' ≤ Multiset.card F
• noInfoLoss : Forest.numEdges F ≤ Forest.numEdges F'

structure Minimalist.MinimalYield {α : Type u_1} {β : Type u_2} (F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) extends Minimalist.MinimalYieldWeak F F' : Prop

The Minimal Yield principle: the weak form plus σ up by exactly one.

• noDivergence : Multiset.card F' ≤ Multiset.card F
• noInfoLoss : Forest.numEdges F ≤ Forest.numEdges F'
• minimalYield : Forest.numNodes F' = Forest.numNodes F + 1

MinimalYieldWeak as a Pareto pullback preorder

def Minimalist.MinimalYield.signature {α : Type u_1} {β : Type u_2} (F : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : ℕᵒᵈ × ℕ

The Pareto signature (b₀ᵒᵈ, α), b₀ dualised so fewer components ranks higher.

Equations

• Minimalist.MinimalYield.signature F = (OrderDual.toDual (Multiset.card F), Forest.numEdges F)

theorem Minimalist.minimalYieldWeak_iff_signature_le {α : Type u_1} {β : Type u_2} {F F' : UnorderedTree.Forest (UnorderedTree (α ⊕ β))} : MinimalYieldWeak F F' ↔ MinimalYield.signature F ≤ MinimalYield.signature F'

def Minimalist.MinimalYieldWeak.pullbackPreorder {α : Type u_1} {β : Type u_2} : Core.Order.PullbackPreorder (UnorderedTree.Forest (UnorderedTree (α ⊕ β))) (ℕᵒᵈ × ℕ)

MinimalYieldWeak packaged as a PullbackPreorder.

Equations

• Minimalist.MinimalYieldWeak.pullbackPreorder = Core.Order.PullbackPreorder.ofProj Minimalist.MinimalYield.signature fun (x x_1 : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) => inferInstance

External Merge

theorem Minimalist.MinimalYield.em_pair {α : Type u_1} {β : Type u_2} (lbl : α) (S S' : UnorderedTree (α ⊕ β)) : MinimalYield {S, S'} {UnorderedTree.node (Sum.inl lbl) {S, S'}}

External Merge of a pair satisfies Minimal Yield: Δb₀ = −1, Δα = +2, Δσ = +1.

Internal Merge

theorem Minimalist.im_pair_size_deltas_deletion {α : Type u_1} {β : Type u_2} (lbl : α) {T mover Q : UnorderedTree (α ⊕ β)} (h : T.numEdges = mover.numEdges + Q.numEdges + 2) : Multiset.card {UnorderedTree.node (Sum.inl lbl) {mover, Q}} = Multiset.card {T} ∧ Forest.numEdges {UnorderedTree.node (Sum.inl lbl) {mover, Q}} = Forest.numEdges {T} ∧ Forest.numNodes {UnorderedTree.node (Sum.inl lbl) {mover, Q}} = Forest.numNodes {T}

Internal Merge via composition leaves b₀, α, σ unchanged (Δᵈ counting): the accessible-term relation α(T) = α(mover) + α(Q) + 2 is MCB eq. 1.6.7.

theorem Minimalist.im_pair_size_deltas_deletion_of_cut {α : Type u_1} {β : Type u_2} (lbl : α) (T : UnorderedTree (α ⊕ β)) (p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) (hp : p ∈ ConnesKreimer.cutSummandsN T) (mover : UnorderedTree (α ⊕ β)) (hcard : p.1 = {mover}) (huc : p.2.numUnary = 1) : Multiset.card {UnorderedTree.node (Sum.inl lbl) {mover, p.2.contractUnary}} = Multiset.card {T} ∧ Forest.numEdges {UnorderedTree.node (Sum.inl lbl) {mover, p.2.contractUnary}} = Forest.numEdges {T} ∧ Forest.numNodes {UnorderedTree.node (Sum.inl lbl) {mover, p.2.contractUnary}} = Forest.numNodes {T}

im_pair_size_deltas_deletion with the α relation discharged from a Δᵈ admissible cut: deleting mover from T and rebinarizing the remainder (contractUnary p.2) leaves b₀, α, σ unchanged. numUnary p.2 = 1 characterizes a single edge cut at a binary node.

theorem Minimalist.im_pair_size_deltas_contraction {α : Type u_1} {β : Type u_2} (lbl : α) {T β_t Q : UnorderedTree (α ⊕ β)} (hβ : β_t.traceLeafCount < β_t.numNodes) (hQ : Q.traceLeafCount < Q.numNodes) (h : T.accessibleCount = β_t.accessibleCount + Q.accessibleCount + 1) : Multiset.card {UnorderedTree.node (Sum.inl lbl) {β_t, Q}} = Multiset.card {T} ∧ Forest.accessibleCount {UnorderedTree.node (Sum.inl lbl) {β_t, Q}} = Forest.accessibleCount {T} + 1 ∧ Forest.accessibleSize {UnorderedTree.node (Sum.inl lbl) {β_t, Q}} = Forest.accessibleSize {T} + 1

Internal Merge via composition leaves b₀ fixed and raises αᶜ, σᶜ by one (Δᶜ counting): the relation αᶜ(T) = αᶜ(β_t) + αᶜ(trunk) + 1 is MCB eq. 1.6.8.

theorem Minimalist.im_pair_size_deltas_contraction_of_cut {α : 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₀)) (β_t : UnorderedTree (α ⊕ β)) (hcard : p.1 = {β_t}) : Multiset.card {UnorderedTree.node (Sum.inl lbl) {β_t, p.2}} = Multiset.card {UnorderedTree.node (Sum.inl a₀) F₀} ∧ Forest.accessibleCount {UnorderedTree.node (Sum.inl lbl) {β_t, p.2}} = Forest.accessibleCount {UnorderedTree.node (Sum.inl a₀) F₀} + 1 ∧ Forest.accessibleSize {UnorderedTree.node (Sum.inl lbl) {β_t, p.2}} = Forest.accessibleSize {UnorderedTree.node (Sum.inl a₀) F₀} + 1

im_pair_size_deltas_contraction with the αᶜ relation discharged from a Δᶜ admissible cut: re-merging an accessible subtree β_t of T = node (inl a₀) F₀ with the contraction quotient p.2 raises αᶜ, σᶜ by one.

Sideward Merge

theorem Minimalist.sideward_2b_b₀_preserved {α : Type u_1} {β : Type u_2} (T_i T_j Tnode T_j_q : UnorderedTree (α ⊕ β)) : Multiset.card {Tnode, T_j_q} = Multiset.card {T_i, T_j}

Sideward Merge of type 2(b) leaves the component count b₀ unchanged.

theorem Minimalist.sideward_3a_b₀_increases {α : Type u_1} {β : Type u_2} (T_i Tnode T_iq : UnorderedTree (α ⊕ β)) : Multiset.card {Tnode, T_iq} = Multiset.card {T_i} + 1

Sideward Merge of type 3(a) increases the component count b₀ by one.

theorem Minimalist.sideward_3b_b₀_increases {α : Type u_1} {β : Type u_2} (T_i T_j Tnode T_iq T_jq : UnorderedTree (α ⊕ β)) : Multiset.card {Tnode, T_iq, T_jq} = Multiset.card {T_i, T_j} + 1

Sideward Merge of type 3(b) increases the component count b₀ by one.

theorem Minimalist.MinimalYieldWeak.not_sideward_3a {α : Type u_1} {β : Type u_2} (T_i Tnode T_iq : UnorderedTree (α ⊕ β)) : ¬MinimalYieldWeak {T_i} {Tnode, T_iq}

Sideward Merge of type 3(a) violates the weak Minimal Yield principle (Δb₀ > 0).

theorem Minimalist.MinimalYieldWeak.not_sideward_3b {α : Type u_1} {β : Type u_2} (T_i T_j Tnode T_iq T_jq : UnorderedTree (α ⊕ β)) : ¬MinimalYieldWeak {T_i, T_j} {Tnode, T_iq, T_jq}

Sideward Merge of type 3(b) violates the weak Minimal Yield principle (Δb₀ > 0).

theorem Minimalist.MinimalYield.not_sideward_3a {α : Type u_1} {β : Type u_2} (T_i Tnode T_iq : UnorderedTree (α ⊕ β)) : ¬MinimalYield {T_i} {Tnode, T_iq}

Strong-form corollary of MinimalYieldWeak.not_sideward_3a.

theorem Minimalist.MinimalYield.not_sideward_3b {α : Type u_1} {β : Type u_2} (T_i T_j Tnode T_iq T_jq : UnorderedTree (α ⊕ β)) : ¬MinimalYield {T_i, T_j} {Tnode, T_iq, T_jq}

Strong-form corollary of MinimalYieldWeak.not_sideward_3b.

Unit merge

theorem Minimalist.MinimalYieldWeak.not_unitMerge {α : Type u_1} {β : Type u_2} (T β_t Q : UnorderedTree (α ⊕ β)) : ¬MinimalYieldWeak {T} {β_t, Q}

The unit-merge stage {T} → {β, T/β} violates weak Minimal Yield (Δb₀ > 0).

theorem Minimalist.MinimalYield.not_unitMerge {α : Type u_1} {β : Type u_2} (T β_t Q : UnorderedTree (α ⊕ β)) : ¬MinimalYield {T} {β_t, Q}

Strong-form corollary of MinimalYieldWeak.not_unitMerge.