Sideward Merge: realization + cost-suppression #
@cite{marcolli-chomsky-berwick-2025}
Realizes M-C-B Lemmas 1.4.4 + 1.4.5 (book pp. 54-55) for the three Sideward-flavored cases of §1.4.1, plus the §1.5 cost-suppression theorems showing they vanish in the ε → 0 limit (Prop 1.5.1, p. 60).
Verbatim from MCB §1.4.5 (p. 54) #
Case 2(b) corresponds to a case of Sideward Merge. Here, one obtains in the new workspace F' a component of the form M(T_i, β) and a component of the form T_j/β. Similarly, case 3(b) also represents a case of Sideward Merge, where in the resulting workspace F', one has new components: M(α, β), as well as T_i/α and T_j/β.
Case 3(a) is the "countercyclic-like" Sideward configuration where
both α and β are accessible terms of the same component T_i — the cut
identifying them is a 2-edge cut producing cutForest = {α_t, β}.
Cut identification #
IsSingleEdgeAccessibleCut T_j β c_β↔cutForest c_β = {β}: cut extracting a single accessible term β.IsTwoEdgeAccessibleCut T_i α_t β c↔cutForest c = {α_t, β}: cut extracting two distinct accessible terms (used for case 3(a)).matchingSingleEdgeCuts T β,matchingTwoEdgeCuts T α β: the Finsets of cuts matching the corresponding predicate. Used in the multi-witness sum form of Lemmas 1.4.4 / 1.4.5 (eq. (1.3.3)).
Realization theorems #
For each case 2b, 3a, 3b:
mergeOp_sideward_X_general_pair: the multi-witness double-sum form matching MCB eq. (1.3.3).mergeOp_sideward_X_pair: a unique-witness corollary collapsing the filter set to a singleton{c_β}(or{c_α, c_β}).mergeOp_sideward_X(residual): induction over residual workspaceFhatviamergeOp_factor_out_singleton(fromMerge.External).
Cost-suppression theorems (§4.1) #
Per MCB §1.5 (Minimal Search via ε-weighted derivation cost — rules 1-5 of §1.5.2 with eq. (1.5.1)-(1.5.2), pp. 59-60), Sideward configurations are subdominant and suppressed in the ε → 0 limit because the cost of extracting an accessible term at depth d carries weight ε^d, which goes to 0 strictly faster than the EM cost (= ε^0 = 1) for d > 0.
mergeOp_eps_zero_for_sideward_2b/3a/3b implement the negative direction
(Sideward → 0); the positive direction (IM survives at weight 1) is queued
as Phase 7g — requires extending the ε-weighted substrate with rule 2's
negative-depth weight on the right channel (ε^{-d_v} on T/T_v).
Status #
Realization theorems sorry-free as of 0.230.808 (Phase 7h closed mergeOp_sideward_3b_general_pair). Cost-suppression theorems sorry-free as of 0.230.804.
A CutShape c_β : CutShape T_j identifies an accessible term β when
its forest is the singleton {β} — i.e., the cut extracts exactly β
from T_j as a subforest. This is the substrate predicate corresponding
to "β ∈ Acc(T_j)" in MCB §1.4.1, witnessed at the algebraic level by
the existence of an admissible cut producing β.
Equations
- Minimalist.Merge.IsSingleEdgeAccessibleCut T_j β c_β = (c_β.cutForest = {β})
Instances For
Equations
- Minimalist.Merge.instDecidableIsSingleEdgeAccessibleCut T_j β c_β = id inferInstance
The Finset of all admissible cuts on T whose cutForest equals the
singleton {β}. Used to express MCB Lemma 1.4.4 in its full
multi-witness sum form (eq. (1.3.3)): mergeOp produces a sum over
all matching cuts, not just a unique witness.
Equations
- Minimalist.Merge.matchingSingleEdgeCuts T β = {c : ConnesKreimer.CutShape T | c.cutForest = {β}}
Instances For
The Finset of all 2-edge admissible cuts on T whose cutForest equals
{α_t, β}. Used for MCB Lemma 1.4.5 (Sideward 3(a)) in its full
multi-witness sum form.
Equations
- Minimalist.Merge.matchingTwoEdgeCuts T α_t β = {c : ConnesKreimer.CutShape T | c.cutForest = {α_t, β}}
Instances For
Sideward Merge case 2(b), F̂ = ∅, multi-witness sum form (M-C-B Lemma 1.4.4, p. 54, full eq. (1.3.3)).
mergeOp T_i β on workspace {T_i, T_j} produces a sum over all
admissible cuts c on T_j with cutForest c = {β}, each contributing
forestToHc {.node T_i β} * deletionRightChannel (remainderDeletion c).
This is MCB's Lemma 1.4.4 in its full algebraic form (sum over
matchings); the unique-witness mergeOp_sideward_2b_pair below
follows as a corollary when matchingSingleEdgeCuts T_j β = {c_β}.
Sideward Merge case 2(b) realization, F̂ = ∅ subcase, didactic
unique-witness form. Quick corollary of mergeOp_sideward_2b_general_pair
when β has a UNIQUE matching cut c_β on T_j. The unique-witness
framing is convenient for analyst-supplied derivations but is not
in M-C-B Lemma 1.4.4 (which sums over all matching cuts per eq. (1.3.3)).
For MCB-faithful claims, prefer the _general_pair form above.
Sideward Merge case 2(b) realization, full residual workspace
(M-C-B Lemma 1.4.4, p. 54). Generalization of mergeOp_sideward_2b_pair
to arbitrary residual workspace Fhat via the factor-out pattern.
The existing mergeOp_factor_out_singleton is parametric in (S, S')
and applies directly to (S, S') = (T_i, β) with
CutAvoidingForest ({T_i, β}) Fhat providing the per-spectator disjointness.
Sideward Merge case 3(b), F̂ = ∅, multi-witness sum form (M-C-B Lemma 1.4.4, p. 54, full eq. (1.3.3)).
mergeOp α_t β on {T_i, T_j} produces the double sum over all
matching α-cuts on T_i and matching β-cuts on T_j. Output:
forestToHc {.node α β} * (∑ α-cuts) * (∑ β-cuts)
where the two sums are over matchingSingleEdgeCuts T_i α_t and
matchingSingleEdgeCuts T_j β respectively. The unique-witness
mergeOp_sideward_3b_pair follows when both filter sets are
singletons.
Sideward Merge case 3(b) realization, F̂ = ∅ subcase, didactic
unique-witness form. Quick corollary of mergeOp_sideward_3b_general_pair
when both α (in T_i) and β (in T_j) have UNIQUE matching cuts
c_α, c_β. The unique-witness framing is convenient for analyst-
supplied derivations but is not in M-C-B Lemma 1.4.4 (which sums
over all matching cuts per eq. (1.3.3)). For MCB-faithful claims,
prefer the _general_pair form above.
Sideward Merge case 3(b) realization, full residual workspace
(M-C-B Lemma 1.4.4, p. 54). Generalization of mergeOp_sideward_3b_pair
via the factor-out pattern, parameterised on (S, S') = (α_t, β).
Sideward Merge case 3(a) realization ("Countercyclic-like Merge",
M-C-B Lemma 1.4.5, p. 55). Both α and β are disjoint accessible terms
of the same component T_i. The operator δ_{α, β} selects
T_v ⊔ T_w ⊗ (T_i/(T_v ⊔ T_w) ⊔ F̂), producing
{M(α, β), T_i/(α ⊔ β)} + Fhat.
Proof strategy: the surviving cross-term comes from a single
2-edge admissible cut on T_i (extracting both α ≃ T_v and
β ≃ T_w as separate subforest elements), yielding cutForest = {α, β} as a 2-element multiset. This requires the substrate
extension IsTwoEdgeAccessibleCut T_i α β c (hypothesis below):
a cut whose cutForest contains exactly α and β as distinct
elements. The mergePost cross-term selection criterion then becomes
cutForest c = {α, β}.
Equations
- Minimalist.Merge.IsTwoEdgeAccessibleCut T_i α_t β c = (c.cutForest = {α_t, β})
Instances For
Equations
- Minimalist.Merge.instDecidableIsTwoEdgeAccessibleCut T_i α_t β c = id inferInstance
Sideward Merge case 3(a), F̂ = ∅, multi-witness sum form (M-C-B Lemma 1.4.5, p. 55, full eq. (1.3.3)).
mergeOp α_t β on workspace {T_i} produces a sum over all
2-edge admissible cuts c on T_i with cutForest c = {α_t, β},
each contributing forestToHc {.node α_t β} * deletionRightChannel (remainderDeletion c). The unique-witness mergeOp_sideward_3a_pair
follows as a corollary.
Sideward Merge case 3(a) realization, F̂ = ∅ subcase, didactic
unique-witness form. Quick corollary of mergeOp_sideward_3a_general_pair
when the 2-edge cut producing {α_t, β} is uniquely witnessed by c.
The unique-witness framing is convenient for analyst-supplied derivations
but is not in M-C-B Lemma 1.4.5 (which sums over all matching 2-edge
cuts per eq. (1.3.3)). For MCB-faithful claims, prefer the _general_pair
form above.
Sideward Merge case 3(a) realization, full residual workspace
(M-C-B Lemma 1.4.5, p. 55). Generalization of mergeOp_sideward_3a_pair
via the factor-out pattern, parameterised on (S, S') = (α_t, β).
Cost-suppression for Sideward 2(b) (MCB §1.5.3 + §1.4.5).
At ε = 0, applying mergeOp_eps 0 T_i β to the workspace
{T_i, T_j} (where β is an accessible term of T_j, not a component)
yields 0 — the Sideward 2(b) realization of mergeOp (which
consumes the cut producing β) is entirely absent at ε = 0 because
comulTreeDel_eps 0 T_j reduces to the primitive part
(T_j ⊗ 1) + (1 ⊗ T_j) (no cut subforests).
No primitive cross-term of (prim T_i) × (prim T_j) has LEFT-channel
forest equal to {T_i, β} (since β ∉ {T_i, T_j} when β ≠ T_i and
β ≠ T_j); mergePost annihilates all four.
Cost-suppression for Sideward 3(a) (MCB §1.5.3 + §1.4.6).
At ε = 0, applying mergeOp_eps 0 α_t β to the single-component
workspace {T_i} (where α_t, β are accessible terms of T_i) yields
0. Same reasoning: at ε = 0 only the primitive part of
comulTreeDel_eps 0 T_i = (T_i ⊗ 1) + (1 ⊗ T_i) survives; neither
primitive contributes LEFT = {α_t, β}.
Cost-suppression for Sideward 3(b) (MCB §1.5.3 + §1.4.5).
At ε = 0, applying mergeOp_eps 0 α_t β to a 2-component workspace
{T_i, T_j} where α_t ∈ Acc(T_i), β ∈ Acc(T_j) yields 0. Same
reasoning as 2(b): only primitive parts survive at ε = 0, and no
primitive cross-term has LEFT = {α_t, β}.