Minimal Search as a weighting of Merge

The ε-weighted Merge M^ε = ⊔ ∘ (Bᵉ ⊗ id) ∘ δ ∘ Δ scales the graft by ε^c, where c is the Minimal-Search cost of the merge. Since mergePost is linear and the graft is its only creation, this is the Δ^c Merge mergeOpC scaled by epsWeight ε c. The net cost is the signed sum of the operands' depth-costs (Cut.extractionCost, Cut.quotientCost): External Merge costs 0; Internal Merge's extraction +d and its own quotient's −d cancel; Sideward Merge's extraction is uncancelled, so c = d > 0. At ε = 0 External and Internal Merge survive and Sideward Merge is annihilated.

Main definitions

• Minimalist.Merge.epsWeight: the weight ε^c.
• Minimalist.Merge.emNetCost, imNetCost, swNetCost: the per-case net costs.
• Minimalist.Merge.mergeOpCEps: the ε-weighted Δ^c Merge.

Main results

• Minimalist.Merge.mergeOpCEps_zero_em, mergeOpCEps_zero_im, mergeOpCEps_zero_sideward: the ε → 0 limit keeps External and Internal Merge and kills Sideward Merge.

References

• [marcolli-chomsky-berwick-2025], §1.5 (Proposition 1.5.1)

The weight

def Minimalist.Merge.epsWeight {R : Type u_1} [CommSemiring R] (ε : R) (c : ℕ) : R

The Minimal-Search ε-weight of a merge with net cost c: ε^c (MCB eq 1.5.2).

Equations

• Minimalist.Merge.epsWeight ε c = ε ^ c

@[simp]

theorem Minimalist.Merge.epsWeight_zero_zero {R : Type u_1} [CommSemiring R] : epsWeight 0 0 = 1

theorem Minimalist.Merge.epsWeight_zero_of_pos {R : Type u_1} [CommSemiring R] {c : ℕ} (hc : 0 < c) : epsWeight 0 c = 0

@[simp]

theorem Minimalist.Merge.epsWeight_one {R : Type u_1} [CommSemiring R] (c : ℕ) : epsWeight 1 c = 1

Signed depth costs of a cut

def Minimalist.Merge.Cut.extractionCost {α : Type u_2} {β : Type u_3} (p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : ℤ

Cut.extractionCost p = depthC p: pulling out the crown of a Δ^c cut costs its depth.

Equations

• Minimalist.Merge.Cut.extractionCost p = ↑(ConnesKreimer.Cut.depthC p)

def Minimalist.Merge.Cut.quotientCost {α : Type u_2} {β : Type u_3} (p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : ℤ

Cut.quotientCost p = −depthC p: the contraction quotient of a Δ^c cut costs minus its depth.

Equations

• Minimalist.Merge.Cut.quotientCost p = -↑(ConnesKreimer.Cut.depthC p)

theorem Minimalist.Merge.Cut.extractionCost_add_quotientCost {α : Type u_2} {β : Type u_3} (p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : extractionCost p + quotientCost p = 0

Re-merging an extracted crown with its own quotient costs nothing.

theorem Minimalist.Merge.Cut.extractionCost_pos {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (a₀ : α) (hT : T.rootValue = Sum.inl a₀) (p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) (hp : p ∈ ConnesKreimer.cutSummandsCN τ T) (hproper : p.1 ≠ 0) : 0 < extractionCost p

Extracting a proper crown from a lexical-rooted object has positive cost.

Net costs and the weighted operator

def Minimalist.Merge.emNetCost : ℕ

External Merge net cost (MCB rule 4, whole operands): 0.

Equations

• Minimalist.Merge.emNetCost = 0

def Minimalist.Merge.imNetCost {α : Type u_2} {β : Type u_3} (p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : ℕ

Internal Merge net cost (MCB Prop 1.5.1, IM): the extracted crown's +d and its own quotient's −d cancel — the signed sum over the same cut p, truncated to ℕ (it is 0, see imNetCost_eq_zero).

Equations

• Minimalist.Merge.imNetCost p = (Minimalist.Merge.Cut.extractionCost p + Minimalist.Merge.Cut.quotientCost p).toNat

def Minimalist.Merge.swNetCost {α : Type u_2} {β : Type u_3} (p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : ℕ

Sideward Merge net cost (MCB Prop 1.5.1, Sideward 2b): the extracted crown's +d, with no quotient operand to cancel it. Equals Cut.depthC p.

Equations

• Minimalist.Merge.swNetCost p = (Minimalist.Merge.Cut.extractionCost p).toNat

@[simp]

theorem Minimalist.Merge.imNetCost_eq_zero {α : Type u_2} {β : Type u_3} (p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : imNetCost p = 0

@[simp]

theorem Minimalist.Merge.swNetCost_eq_depthC {α : Type u_2} {β : Type u_3} (p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) : swNetCost p = ConnesKreimer.Cut.depthC p

theorem Minimalist.Merge.swNetCost_pos {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (a₀ : α) (hT : T.rootValue = Sum.inl a₀) (p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) (hp : p ∈ ConnesKreimer.cutSummandsCN τ T) (hproper : p.1 ≠ 0) : 0 < swNetCost p

A Sideward Merge of a lexical-rooted object has strictly positive net cost (MCB Prop 1.5.1) — the uncancelled extraction depth.

noncomputable def Minimalist.Merge.mergeOpCEps {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [DecidableEq (UnorderedTree (α ⊕ β))] (τ : UnorderedTree (α ⊕ β) → β) (ε : R) (c : ℕ) (lbl : α ⊕ β) (S S' : UnorderedTree (α ⊕ β)) : ConnesKreimer R (UnorderedTree (α ⊕ β)) →ₗ[R] ConnesKreimer R (UnorderedTree (α ⊕ β))

The ε-weighted Δ^c Merge operator (MCB §1.5, eq 1.5.2): the Δ^c merge scaled by the Minimal-Search weight ε^c.

Equations

• Minimalist.Merge.mergeOpCEps τ ε c lbl S S' = Minimalist.Merge.epsWeight ε c • Minimalist.Merge.mergeOpC τ lbl S S'

@[simp]

theorem Minimalist.Merge.mergeOpCEps_one {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [DecidableEq (UnorderedTree (α ⊕ β))] (τ : UnorderedTree (α ⊕ β) → β) (c : ℕ) (lbl : α ⊕ β) (S S' : UnorderedTree (α ⊕ β)) : mergeOpCEps τ 1 c lbl S S' = mergeOpC τ lbl S S'

At ε = 1 the weight is trivial and mergeOpCEps recovers the unweighted Δ^c Merge.

@[simp]

theorem Minimalist.Merge.mergeOpCEps_zero_em {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [DecidableEq (UnorderedTree (α ⊕ β))] (τ : UnorderedTree (α ⊕ β) → β) (lbl : α ⊕ β) (S S' : UnorderedTree (α ⊕ β)) : mergeOpCEps τ 0 emNetCost lbl S S' = mergeOpC τ lbl S S'

MCB Prop 1.5.1, External Merge survives ε → 0. EM has net cost 0, so its weight ε^0 = 1 is unaffected: mergeOpCEps τ 0 emNetCost = mergeOpC τ.

@[simp]

theorem Minimalist.Merge.mergeOpCEps_zero_im {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [DecidableEq (UnorderedTree (α ⊕ β))] (τ : UnorderedTree (α ⊕ β) → β) (p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) (lbl : α ⊕ β) (S S' : UnorderedTree (α ⊕ β)) : mergeOpCEps τ 0 (imNetCost p) lbl S S' = mergeOpC τ lbl S S'

MCB Prop 1.5.1, Internal Merge survives ε → 0. IM has net cost 0 — the extraction +d and its own quotient's −d cancel — so its weight is 1 and the operator is preserved at ε = 0.

theorem Minimalist.Merge.mergeOpCEps_zero_sideward {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [DecidableEq (UnorderedTree (α ⊕ β))] (τ : UnorderedTree (α ⊕ β) → β) {c : ℕ} (hc : 0 < c) (lbl : α ⊕ β) (S S' : UnorderedTree (α ⊕ β)) : mergeOpCEps τ 0 c lbl S S' = 0

MCB Prop 1.5.1, Sideward Merge vanishes ε → 0. A Sideward Merge has net cost > 0 (the uncancelled extraction depth), so its weight ε^{>0} = 0 at ε = 0: the operator is annihilated.

theorem Minimalist.Merge.mergeOpCEps_zero_sideward_of_cut {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [DecidableEq (UnorderedTree (α ⊕ β))] (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) (a₀ : α) (hT : T.rootValue = Sum.inl a₀) (p : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) × UnorderedTree (α ⊕ β)) (hp : p ∈ ConnesKreimer.cutSummandsCN τ T) (hproper : p.1 ≠ 0) (lbl : α ⊕ β) (S S' : UnorderedTree (α ⊕ β)) : mergeOpCEps τ 0 (swNetCost p) lbl S S' = 0

MCB Prop 1.5.1, Sideward Merge vanishes — instantiated at an actual Δ^c extraction p of a lexical-rooted object: the uncancelled depth makes swNetCost p > 0, so the operator is annihilated at ε = 0.