Minimal Yield (MCB Definition 1.6.1)

@cite{marcolli-chomsky-berwick-2025} §1.6.1, book p. 63

Realises M-C-B's Minimal Yield principle (Def 1.6.1) as a predicate on forest transformations, plus the per-merge counting characterization of Proposition 1.6.4 (book p. 66) and Proposition 1.6.8 (book p. 69) for the EM/IM/Sideward cases.

Definition (verbatim, MCB Def 1.6.1, book p. 63 + eq. 1.6.2)

A transformation Φ : 𝓕_SO₀ → 𝓕_SO₀ satisfies the Minimal Yield principle if the following conditions hold:

b₀(Φ(F)) ≤ b₀(F) (no divergence) α(Φ(F)) ≥ α(F) (no information loss) σ(Φ(F)) = σ(F) + 1 (minimality of yield)

MCB also implicitly invokes a weak form that drops the third condition (book p. 69 says Sideward 3(a)/3(b) are "ruled out by the Minimal Yield principle, in the strong form (for Δ^c) or in the weak form (for Δ^d)"). We provide both MinimalYield (strong) and MinimalYieldWeak (drops minimalYield).

Per-merge characterization (MCB Prop 1.6.4 + Prop 1.6.8)

Merge	Δb₀	Δα	Δσ	Strong	Weak
External (Δ^c, Δ^d)	−1	+2	+1	✓	✓
Internal w/ Δ^c	0	+1	+1	✓	✓
Internal w/ Δ^d	0	0	0	✗ (Δσ=0)	✓
Sideward 2(b) Δ^c	0	+1	+1	✓	✓
Sideward 2(b) Δ^d	0	0	0	✗ (Δσ=0)	✓
Sideward 3(a) Δ^c	+1	0	+1	✗ (Δb₀>0)	✗ (Δb₀>0)
Sideward 3(a) Δ^d	+1	−2	−1	✗ (Δb₀>0)	✗ (Δb₀>0)
Sideward 3(b) Δ^c	+1	0	+1	✗ (Δb₀>0)	✗ (Δb₀>0)
Sideward 3(b) Δ^d	+1	−2	−1	✗ (Δb₀>0)	✗ (Δb₀>0)

The 3(a)/Δ^d row matches MCB Prop 1.6.8 (book p. 69) for the elementary admissible 2-edge cut on T_a (where numContractions = 2). Our sideward_3a_size_deltas_deltaD proves a strict generalization parameterized by numContractions c_i ∈ {1, 2}, with sideward_3a_size_deltas_deltaD_specific (corollary via numContractions_twoEdge) recovering MCB's stated (+1, −2, −1).

The Sideward 2(b)/Δ^c row is the same as IM/Δ^c for sizes — Remark 1.6.9 (book p. 71) explicitly notes that 2(b) is indistinguishable from IM by sizes alone in either Δ^c or Δ^d. NCL (InducedMapNCL) is what discriminates them.

EM survives both forms unconditionally. IM/Δ^d and Sideward 2(b) produce identical (Δb₀, Δα, Δσ) signatures (Remark 1.6.9, book p. 71) — they are distinguished only by NCL (NoComplexityLoss). Sideward 3(a)/3(b) are ruled out by the strong AND weak forms via Δb₀ > 0 (noDivergence violation).

Out of scope (queued)

• Full (Δα, Δσ) tables for Sideward 2(b)/3(a)/3(b) under Δ^c (need Δ^c substrate; only Δ^d is implemented).
• Sideward NCL negative direction (MCB Prop 1.6.10 negative): linglib's NCLBetween is existential; MCB Def 1.6.2 specifies the unique induced map Φ₀ : π₀(F) → π₀(Φ(F)). Bridging requires either strengthening NCLBetween or adding an InducedMapNCL predicate.
• Per-transformation lifting MinimalYieldTransformation Φ := ∀ F, MinimalYield F (Φ F).

structure Minimalist.Merge.MinimalYieldWeak {α : Type u_1} {β : Type u_2} (F F' : ConnesKreimer.TraceForest α β) : Prop

Minimal Yield principle, weak form (M-C-B Def 1.6.1, book p. 63 parenthetical: "One can consider a weaker form by only requiring the two bounds on b₀ and α."). Used at p. 69 to rule out Sideward 3(a)/3(b) under Δ^d. Keeps noDivergence and noInfoLoss; drops the minimalYield (σ = +1) condition that the strong form has.

• noDivergence : F'.b₀ ≤ F.b₀
• noInfoLoss : F.alpha ≤ F'.alpha

structure Minimalist.Merge.MinimalYield {α : Type u_1} {β : Type u_2} (F F' : ConnesKreimer.TraceForest α β) extends Minimalist.Merge.MinimalYieldWeak F F' : Prop

Minimal Yield principle, strong form (M-C-B Def 1.6.1, book p. 63 + eq. 1.6.2). The strong form extends the weak form by adding the third condition σ(F') = σ(F) + 1 ("minimality of yield"). The toWeak projection is now automatic via MinimalYield.toMinimalYieldWeak.

• noDivergence : F'.b₀ ≤ F.b₀
• noInfoLoss : F.alpha ≤ F'.alpha
• minimalYield : F'.sigma = F.sigma + 1

@[reducible, inline]

abbrev Minimalist.Merge.MinimalYield.toWeak {α : Type u_1} {β : Type u_2} {F F' : ConnesKreimer.TraceForest α β} (h : MinimalYield F F') : MinimalYieldWeak F F'

Strong implies weak (auto-projection alias).

Equations

• ⋯ = ⋯

§0.5: MinimalYieldWeak as a Pareto pullback preorder

The two MinimalYieldWeak conditions are exactly a Pareto comparison on the (b₀ᵒᵈ, α) signature: noDivergence reverses the order on b₀ (smaller is "better"), noInfoLoss keeps α in the natural direction (larger is "better"). Wrapping the relation as a Core.Order.FeaturePreorder exposes this Pareto structure: same shape as Minimalist.DerivationCost.featurePreorder (4-d cost) and Core.Constraint.ConstraintSystem.paretoFeaturePreorder (OT/HG violation profile).

Reflexivity (MYWeak F F) and transitivity (MYWeak F F' → MYWeak F' F'' → MYWeak F F'') come for free as the underlying Preorder.lift instance. The strong form (MinimalYield) drops out of this picture because its σ = +1 constraint is an equality, not a ≤; treat it as MY-Weak plus a separate σ-step witness.

def Minimalist.Merge.MinimalYieldSignature {α : Type u_1} {β : Type u_2} (F : ConnesKreimer.TraceForest α β) : ℕᵒᵈ × ℕ

The Pareto signature for MinimalYieldWeak: pull a forest back to the (b₀ᵒᵈ, α) feature space. The OrderDual on b₀ flips its ≤ so that "smaller b₀" becomes "larger feature" — matching the MCB sign convention where merges that reduce workspace component count are preferred.

Equations

• Minimalist.Merge.MinimalYieldSignature F = (OrderDual.toDual F.b₀, F.alpha)

@[simp]

theorem Minimalist.Merge.minimalYieldWeak_iff_signature_le {α : Type u_1} {β : Type u_2} {F F' : ConnesKreimer.TraceForest α β} : MinimalYieldWeak F F' ↔ MinimalYieldSignature F ≤ MinimalYieldSignature F'

MinimalYieldWeak F F' is exactly the pullback Pareto-≤ on the (b₀ᵒᵈ, α) signature. By OrderDual.toDual_le_toDual := Iff.rfl and Prod's componentwise preorder, this collapses to MYWeak's two ≤ conditions definitionally.

def Minimalist.Merge.minimalYieldWeakFeaturePreorder {α : Type u_1} {β : Type u_2} : Core.Order.FeaturePreorder (ConnesKreimer.TraceForest α β) (ℕᵒᵈ × ℕ)

MinimalYieldWeak packaged as a Core.Order.FeaturePreorder over TraceForest α β, with feature space ℕᵒᵈ × ℕ (Pareto pullback via MinimalYieldSignature). Same shape as Minimalist.DerivationCost.featurePreorder.

Note: not registered as a Preorder TraceForest instance because TraceForest = Multiset already carries other order structures (multiset ⊆); use .toPreorder explicitly when chain reasoning is needed.

Equations

• Minimalist.Merge.minimalYieldWeakFeaturePreorder = Core.Order.FeaturePreorder.ofFeature Minimalist.Merge.MinimalYieldSignature fun (x x_1 : ConnesKreimer.TraceForest α β) => inferInstance

§1: EM Case 1 satisfies MinimalYield (MCB Prop 1.6.4 EM row)

theorem Minimalist.Merge.em_pair_satisfiesMinimalYield {α : Type u_1} {β : Type u_2} (S S' : ConnesKreimer.TraceTree α β) : MinimalYield {S, S'} {S.node S'}

EM Case 1, F̂ = ∅ (MCB Prop 1.6.4 EM row, book p. 66). External Merge of two member components S, S' produces the singleton {.node S S'}. Δb₀ = −1, Δα = +2, Δσ = +1.

§2: IM size deltas under Δ^d (MCB Prop 1.6.4 IM/Δ^d row)

theorem Minimalist.Merge.im_pair_size_deltas_deltaD {α : Type u_1} {β : Type u_2} {T mover Q : ConnesKreimer.TraceTree α β} (h_size : T.size = mover.size + Q.size + 1) : {mover.node Q}.b₀ = {T}.b₀ ∧ {mover.node Q}.alpha = {T}.alpha ∧ {mover.node Q}.sigma = {T}.sigma

IM via composition (Δ^d) (MCB Prop 1.6.4 IM/Δ^d row, book p. 66). Under the size-conservation hypothesis T.size = mover.size + Q.size + 1 (the size analog of cut_leafCount_conservation), IM {T} → {.node mover Q} preserves all three measures: Δb₀ = 0, Δα = 0, Δσ = 0.

IM under Δ^d satisfies MinimalYieldWeak but NOT MinimalYield (the strong form requires Δσ = +1; under Δ^c IM gives Δσ = +1 instead). See MCB Remark 1.6.6 (book p. 67) on the Δ^c vs Δ^d counting difference.

The hypothesis h_size : T.size = mover.size + Q.size + 1 is the size analog of cut_leafCount_conservation; im_pair_size_deltas_deltaD_of_cut below discharges it from a single-edge cut on T.

theorem Minimalist.Merge.im_pair_size_deltas_deltaD_of_cut {α : Type u_1} {β : Type u_2} {T mover Q : ConnesKreimer.TraceTree α β} (c : ConnesKreimer.CutShape T) (h_cf : c.cutForest = {mover}) (h_rd : c.remainderDeletion = some Q) : {mover.node Q}.b₀ = {T}.b₀ ∧ {mover.node Q}.alpha = {T}.alpha ∧ {mover.node Q}.sigma = {T}.sigma

IM via composition (Δ^d), discharged from cut data: drop the h_size hypothesis from im_pair_size_deltas_deltaD by deriving it from a single-edge cut on T (c.cutForest = {mover}, c.remainderDeletion = some Q). Uses CutShape.singleEdgeCut_size_relation.

§2.5: IM size deltas under Δ^c (MCB Prop 1.6.4 IM/Δ^c row)

theorem Minimalist.Merge.im_pair_size_deltas_contraction {α : Type u_1} {β : Type u_2} [Inhabited β] {T β_t : ConnesKreimer.TraceTree α β} (c : ConnesKreimer.CutShape T) (h_tf : T.nonTraceSize = T.size) (h_cf : c.cutForest = {β_t}) : {β_t.node c.remainder}.b₀ = {T}.b₀ ∧ {β_t.node c.remainder}.alphaC = {T}.alphaC + 1 ∧ {β_t.node c.remainder}.sigmaC = {T}.sigmaC + 1

IM via composition (Δ^c) (MCB Prop 1.6.4 IM/Δ^c row, book p. 66). For a single-edge cut c on a trace-free T extracting β_t, the Δ^c-IM workspace transformation {T} → {.node β_t (T/^c β_t)} increases αᶜ and σᶜ by exactly 1: Δb₀ = 0, Δαᶜ = +1, Δσᶜ = +1.

Contrast with IM/Δ^d (im_pair_size_deltas_deltaD): Δ^d keeps both measures at 0, while Δ^c shows the +1 increase that distinguishes IM from EM in MCB's preferred (Δ^c) counting. The trace marker in T/^c β_t is correctly EXCLUDED from αᶜ via accCountC (MCB's "cancellation of the deeper copy").

§3: Sideward Minimal Yield analysis (MCB Prop 1.6.8 + Remark 1.6.9)

theorem Minimalist.Merge.sideward_2b_b₀_preserved {α : Type u_1} {β : Type u_2} (T_i T_j Tnode T_j_q : ConnesKreimer.TraceTree α β) : {Tnode, T_j_q}.b₀ = {T_i, T_j}.b₀

Sideward 2(b) preserves b₀ (MCB Prop 1.6.8 2(b) row, book p. 69). Workspace {T_i, T_j} → {.node T_i β, T_j/β} retains 2 components.

theorem Minimalist.Merge.sideward_2b_size_deltas_deltaD {α : Type u_1} {β : Type u_2} {T_i T_j β_t Tnode T_j_q : ConnesKreimer.TraceTree α β} (h_size : T_j.size = β_t.size + T_j_q.size + 1) (h_node : Tnode.size = T_i.size + β_t.size + 1) : {Tnode, T_j_q}.b₀ = {T_i, T_j}.b₀ ∧ {Tnode, T_j_q}.alpha = {T_i, T_j}.alpha ∧ {Tnode, T_j_q}.sigma = {T_i, T_j}.sigma

Sideward 2(b) (Δα, Δσ) deltas under size conservation (MCB Prop 1.6.8 2(b)/Δ^d row, book p. 69). Under h_size : T_j.size = β_t.size + T_j_q.size + 1 (the size-conservation hypothesis on the cut producing β_t from T_j) AND h_node : Tnode.size = T_i.size + β_t.size + 1 (the merged-node size relation, automatic when Tnode = .node T_i β_t), Sideward 2(b) preserves α and σ:

Measure	Before {T_i, T_j}	After {Tnode, T_j_q}	Δ
b₀	2	2	0
α	(T_i.size − 1) + (T_j.size − 1)	Tnode.size − 1 + T_j_q.size − 1	0
σ	2 + α(F)	2 + α(F)	0

Realises Remark 1.6.9 (book p. 71): "the Sideward Merge of type 2(b) cannot be distinguished solely in terms of its effect on the sizes b₀, α, and σ from Internal Merge." Both produce (0, 0, 0). NCL (NCLBetween) is what discriminates them.

The tree variable is named β_t (per Sideward.lean convention) to avoid clashing with the type-level β : Type* from the file's variable declaration. MCB's notation β (as in eq. 1.6.7-1.6.10) corresponds.

theorem Minimalist.Merge.sideward_2b_size_deltas_deltaD_of_cut {α : Type u_1} {β : Type u_2} {T_i T_j β_t T_j_q : ConnesKreimer.TraceTree α β} (c : ConnesKreimer.CutShape T_j) (h_cf : c.cutForest = {β_t}) (h_rd : c.remainderDeletion = some T_j_q) : {T_i.node β_t, T_j_q}.b₀ = {T_i, T_j}.b₀ ∧ {T_i.node β_t, T_j_q}.alpha = {T_i, T_j}.alpha ∧ {T_i.node β_t, T_j_q}.sigma = {T_i, T_j}.sigma

Sideward 2(b) (Δα, Δσ) deltas, discharged from cut data: drop both h_size and h_node hypotheses from sideward_2b_size_deltas_deltaD. h_size comes from a single-edge cut c on T_j extracting β_t and leaving T_j_q; h_node from Tnode = .node T_i β_t (so size_node gives the size relation).

theorem Minimalist.Merge.sideward_2b_size_deltas_contraction {α : Type u_1} {β : Type u_2} [Inhabited β] {T_i T_j β_t : ConnesKreimer.TraceTree α β} (c : ConnesKreimer.CutShape T_j) (h_T_j_tf : T_j.nonTraceSize = T_j.size) (h_T_i_tf : T_i.nonTraceSize = T_i.size) (h_cf : c.cutForest = {β_t}) : {T_i.node β_t, c.remainder}.b₀ = {T_i, T_j}.b₀ ∧ {T_i.node β_t, c.remainder}.alphaC = {T_i, T_j}.alphaC + 1 ∧ {T_i.node β_t, c.remainder}.sigmaC = {T_i, T_j}.sigmaC + 1

Sideward 2(b) under Δ^c (MCB Prop 1.6.8 2(b)/Δ^c row, book p. 69). {T_i, T_j} → {.node T_i β_t, T_j/^c β_t} for a single-edge cut on trace-free T_j extracting β_t. Δb₀ = 0, Δαᶜ = +1, Δσᶜ = +1.

Like IM/Δ^c, the trace marker in the contraction-quotient is excluded from αᶜ per MCB's Lemma 1.6.3 eq. 1.6.8.

theorem Minimalist.Merge.sideward_3a_b₀_increases {α : Type u_1} {β : Type u_2} (T_i Tnode T_iq : ConnesKreimer.TraceTree α β) : {Tnode, T_iq}.b₀ = {T_i}.b₀ + 1

Sideward 3(a) increases b₀ by 1 (MCB Prop 1.6.8 3(a) row, book p. 69). Workspace {T_i} → {.node α β, T_i/(α⊔β)}: 1 component becomes 2.

theorem Minimalist.Merge.sideward_3b_b₀_increases {α : Type u_1} {β : Type u_2} (T_i T_j Tnode T_iq T_jq : ConnesKreimer.TraceTree α β) : {Tnode, T_iq, T_jq}.b₀ = {T_i, T_j}.b₀ + 1

Sideward 3(b) increases b₀ by 1 (MCB Prop 1.6.8 3(b) row, book p. 69). Workspace {T_i, T_j} → {.node α β, T_i/α, T_j/β}: 2 components become 3.

theorem Minimalist.Merge.sideward_3b_size_deltas_deltaD {α : Type u_1} {β : Type u_2} {T_i T_j a b T_iq T_jq : ConnesKreimer.TraceTree α β} (h_i : T_i.size = a.size + T_iq.size + 1) (h_j : T_j.size = b.size + T_jq.size + 1) : {a.node b, T_iq, T_jq}.b₀ = {T_i, T_j}.b₀ + 1 ∧ {a.node b, T_iq, T_jq}.alpha + 2 = {T_i, T_j}.alpha ∧ {a.node b, T_iq, T_jq}.sigma + 1 = {T_i, T_j}.sigma

Sideward 3(b) full (Δb₀, Δα, Δσ) under Δ^d (MCB Prop 1.6.8 3(b) row, book p. 69 — full table). Workspace {T_i, T_j} → {.node a b, T_iq, T_jq} where T_iq is the deletion-quotient of a single-edge cut on T_i extracting a, and similarly for T_jq from T_j extracting b.

Measure	Before	After	Δ
b₀	2	3	+1
α	(T_i.size − 1) + (T_j.size − 1)	(.node a b).size − 1 + (T_iq − 1) + (T_jq − 1)	−2
σ	2 + α(F)	3 + α(F) − 2	−1

Δb₀ = +1 alone rules out Sideward 3(b) (sideward_3b_violates_noDivergenceWeak); here we record the full numerical signature for Remark 1.6.9-style discrimination.

theorem Minimalist.Merge.sideward_3b_size_deltas_deltaD_of_cut {α : Type u_1} {β : Type u_2} {T_i T_j a b T_iq T_jq : ConnesKreimer.TraceTree α β} (c_i : ConnesKreimer.CutShape T_i) (h_cf_i : c_i.cutForest = {a}) (h_rd_i : c_i.remainderDeletion = some T_iq) (c_j : ConnesKreimer.CutShape T_j) (h_cf_j : c_j.cutForest = {b}) (h_rd_j : c_j.remainderDeletion = some T_jq) : {a.node b, T_iq, T_jq}.b₀ = {T_i, T_j}.b₀ + 1 ∧ {a.node b, T_iq, T_jq}.alpha + 2 = {T_i, T_j}.alpha ∧ {a.node b, T_iq, T_jq}.sigma + 1 = {T_i, T_j}.sigma

Sideward 3(b) full deltas, discharged from cut data: drop both h_i and h_j size hypotheses by deriving them from single-edge cuts c_i on T_i and c_j on T_j.

Sideward 3(a): two-edge cut full deltas

theorem Minimalist.Merge.sideward_3a_size_deltas_deltaD {α : Type u_1} {β : Type u_2} {T_i a b T_iq : ConnesKreimer.TraceTree α β} (c_i : ConnesKreimer.CutShape T_i) (h_cf : c_i.cutForest = {a, b}) (h_rd : c_i.remainderDeletion = some T_iq) : {a.node b, T_iq}.b₀ = {T_i}.b₀ + 1 ∧ {a.node b, T_iq}.alpha + c_i.numContractions = {T_i}.alpha ∧ {a.node b, T_iq}.sigma + c_i.numContractions = {T_i}.sigma + 1

Sideward 3(a) full (Δb₀, Δα, Δσ) under Δ^d (MCB Prop 1.6.8 3(a) row, book p. 69 — full table, parameterized by contraction count).

Workspace {T_i} → {.node a b, T_iq} where T_iq is the deletion- quotient of a TWO-edge cut c_i on T_i extracting both a and b.

The cut's numContractions c_i depends on the relative position of the two extracted subtrees in T_i:

• 1 contraction if a, b are siblings (single .bothCut)
• 2+ contractions otherwise (the two cut paths each contract a parent)

Hence Δα and Δσ "vary" per MCB's prose, but the variation is captured by numContractions c_i:

Measure	Before	After	Δ
b₀	1	2	+1
α	T_i.size − 1	(a + b) + (T_iq − 1)	−numContractions c_i
σ	T_i.size	1 + a + b + T_iq	1 − numContractions c_i

Δb₀ = +1 alone rules out 3(a) (sideward_3a_violates_noDivergenceWeak); here we record the full numerical signature parameterized by the cut's contraction count, derivable from cut_size_conservation.

theorem Minimalist.Merge.sideward_3a_size_deltas_deltaD_specific {α : Type u_1} {β : Type u_2} {T_i a b T_iq : ConnesKreimer.TraceTree α β} (c_i : ConnesKreimer.CutShape T_i) (h_cf : c_i.cutForest = {a, b}) (h_rd : c_i.remainderDeletion = some T_iq) : {a.node b, T_iq}.b₀ = {T_i}.b₀ + 1 ∧ {a.node b, T_iq}.alpha + 2 = {T_i}.alpha ∧ {a.node b, T_iq}.sigma + 1 = {T_i}.sigma

Sideward 3(a), MCB-specific (+1, −2, −1) form (Prop 1.6.8 3(a)/Δ^d row, book p. 69 — table form). MCB's proof (book p. 70) restricts to a genuine 2-edge cut leaving a non-trivial deletion-quotient T_iq; in that setting numContractions c_i = 2 always (sibling extractions pass through .bothCut collapsing the parent → 1 contraction; separated paths give 2 contractions; either way for the hypothesis cutForest.card = 2 ∧ remainderDeletion = some _ we get exactly 2, by numContractions_twoEdge).

theorem Minimalist.Merge.sideward_3a_size_deltas_contraction {α : Type u_1} {β : Type u_2} [Inhabited β] {T_i a b : ConnesKreimer.TraceTree α β} (c_i : ConnesKreimer.CutShape T_i) (h_T_i_tf : T_i.nonTraceSize = T_i.size) (h_cf : c_i.cutForest = {a, b}) : {a.node b, c_i.remainder}.b₀ = {T_i}.b₀ + 1 ∧ {a.node b, c_i.remainder}.alphaC = {T_i}.alphaC ∧ {a.node b, c_i.remainder}.sigmaC = {T_i}.sigmaC + 1

Sideward 3(a) under Δ^c (MCB Prop 1.6.8 3(a)/Δ^c row, book p. 69). For a 2-edge cut on trace-free T_i extracting a and b: Δb₀ = +1, Δαᶜ = 0, Δσᶜ = +1. (Δb₀ = +1 still rules out 3(a) under Minimal Yield even with Δ^c counting.)

theorem Minimalist.Merge.sideward_3b_size_deltas_contraction {α : Type u_1} {β : Type u_2} [Inhabited β] {T_i T_j a b : ConnesKreimer.TraceTree α β} (c_i : ConnesKreimer.CutShape T_i) (h_T_i_tf : T_i.nonTraceSize = T_i.size) (h_cf_i : c_i.cutForest = {a}) (c_j : ConnesKreimer.CutShape T_j) (h_T_j_tf : T_j.nonTraceSize = T_j.size) (h_cf_j : c_j.cutForest = {b}) : {a.node b, c_i.remainder, c_j.remainder}.b₀ = {T_i, T_j}.b₀ + 1 ∧ {a.node b, c_i.remainder, c_j.remainder}.alphaC = {T_i, T_j}.alphaC ∧ {a.node b, c_i.remainder, c_j.remainder}.sigmaC = {T_i, T_j}.sigmaC + 1

Sideward 3(b) under Δ^c (MCB Prop 1.6.8 3(b)/Δ^c row, book p. 69). For single-edge cuts c_i on trace-free T_i extracting a and c_j on trace-free T_j extracting b: Δb₀ = +1, Δαᶜ = 0, Δσᶜ = +1.

theorem Minimalist.Merge.sideward_3a_violates_noDivergenceWeak {α : Type u_1} {β : Type u_2} (T_i Tnode T_iq : ConnesKreimer.TraceTree α β) : ¬MinimalYieldWeak {T_i} {Tnode, T_iq}

Sideward 3(a) violates MinimalYieldWeak.noDivergence (a fortiori violates the strong form). Δb₀ = +1 rules out Sideward 3(a) under either form.

theorem Minimalist.Merge.sideward_3b_violates_noDivergenceWeak {α : Type u_1} {β : Type u_2} (T_i T_j Tnode T_iq T_jq : ConnesKreimer.TraceTree α β) : ¬MinimalYieldWeak {T_i, T_j} {Tnode, T_iq, T_jq}

Sideward 3(b) violates MinimalYieldWeak.noDivergence (a fortiori violates the strong form). Δb₀ = +1 rules out Sideward 3(b).

theorem Minimalist.Merge.sideward_3a_violates_noDivergence {α : Type u_1} {β : Type u_2} (T_i Tnode T_iq : ConnesKreimer.TraceTree α β) : ¬MinimalYield {T_i} {Tnode, T_iq}

Strong-form corollary of sideward_3a_violates_noDivergenceWeak.

theorem Minimalist.Merge.sideward_3b_violates_noDivergence {α : Type u_1} {β : Type u_2} (T_i T_j Tnode T_iq T_jq : ConnesKreimer.TraceTree α β) : ¬MinimalYield {T_i, T_j} {Tnode, T_iq, T_jq}

Strong-form corollary of sideward_3b_violates_noDivergenceWeak.

§4: Unit-merge violation (MCB Remark 1.6.7, book p. 67)

theorem Minimalist.Merge.unitMerge_violates_noDivergenceWeak {α : Type u_1} {β : Type u_2} (T β_t Q : ConnesKreimer.TraceTree α β) : ¬MinimalYieldWeak {T} {β_t, Q}

M_{S,1} alone violates MinimalYield (MCB Remark 1.6.7, book p. 67). The unit-merge stage of IM via composition transforms {T} → {β, T/β} (extracting an accessible term β from T, leaving the deletion-quotient Q = T/β as the other component). Δb₀ = +1 violates noDivergence.

MCB's argument: this shows M_{S,1} cannot occur standalone as a Merge operation — it can occur only in the composition M_{β, T/β} ∘ M_{β, 1} that gives Internal Merge (Prop 1.4.2). The "virtual particles" caveat in Internal.lean §4 corresponds to this same observation.

Proof: structurally identical to sideward_3a_b₀_increases — {T} → {β, T/β} is one-component-in, two-components-out.

theorem Minimalist.Merge.unitMerge_violates_noDivergence {α : Type u_1} {β : Type u_2} (T β_t Q : ConnesKreimer.TraceTree α β) : ¬MinimalYield {T} {β_t, Q}

Strong-form corollary of unitMerge_violates_noDivergenceWeak.