Sideward Merge: realization on the canonical carrier #
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 on the canonical carrier
ConnesKreimer R (Nonplanar α), using the Δ^ρ deletion coproduct
comulAlgHomN (cuts are the cutSummandsN multiset; crowns are
Forest (Nonplanar α), remainders bare Nonplanar α).
Cut identification #
A cut of T is a summand p ∈ cutSummandsN T with crown p.1 and
remainder p.2. The matching multisets pick the cuts whose crown is a
prescribed accessible-term forest:
matchingSingleEdgeCutsN T β: cuts withp.1 = {β}(single accessible term β).matchingTwoEdgeCutsN T α_t β: cuts withp.1 = {α_t, β}(two accessible terms, case 3(a)).
Realization theorems #
For each case 2b, 3a, 3b:
mergeOp_sideward_X_general_pair: the multi-witness sum form matching MCB eq. (1.3.3) — a sum (or double sum) over all matching cuts.mergeOp_sideward_X_pair: a unique-witness corollary collapsing the matching multiset to a singleton{p0}.mergeOp_sideward_X(residual): induction over residual workspaceFhatviamergeOp_factor_out_singleton(fromMerge.External), underCutAvoidingForestN.
Deferred (substrate gap) #
The §1.5 cost-suppression theorems (mergeOp_eps_zero_for_sideward_*,
showing Sideward configurations vanish in the ε → 0 Minimal-Search limit)
ride the same ε-weighted Δ^ρ gap as External/Internal's ε arc: there
is no cutTotalDepth analogue on cutSummandsN yet. They are queued
behind that substrate and omitted here.
Matching-cut multisets #
Cut summands of T whose crown forest is the singleton {β} (single
accessible-term extraction). The cutSummandsN analogue of legacy
matchingSingleEdgeCuts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cut summands of T whose crown forest is {α_t, β} (two accessible
terms, case 3(a)). The cutSummandsN analogue of legacy
matchingTwoEdgeCuts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Sum-reduction helpers #
Case 2(b): one component contributes M(T_i, β), the other T_j/β #
Sideward Merge case 2(b), F̂ = ∅, multi-witness sum form (M-C-B Lemma 1.4.4, p. 54, eq. (1.3.3)).
mergeOp lbl T_i β on {T_i, T_j} produces a sum over all cuts of
T_j whose crown is {β}, each contributing of' {M(T_i, β)} * ofTree (T_j/β). Only the prim T_i × cut T_j cross-term survives; the other
three vanish.
Sideward Merge case 2(b) realization, F̂ = ∅, unique-witness form.
Corollary of mergeOp_sideward_2b_general_pair when β has a unique
matching cut p0 on T_j (the matching multiset is {p0}).
Sideward Merge case 2(b) realization, full residual workspace (M-C-B
Lemma 1.4.4, p. 54). Generalization of mergeOp_sideward_2b_pair via the
factor-out pattern, parameterised on (S, S') = (T_i, β).
Case 3(b): M(α, β) plus T_i/α and T_j/β #
Sideward Merge case 3(b), F̂ = ∅, multi-witness double-sum form (M-C-B Lemma 1.4.4, p. 54, eq. (1.3.3)).
mergeOp lbl α_t β on {T_i, T_j} produces the double sum over all
{α_t}-cuts of T_i and {β}-cuts of T_j. Only the cut × cut
cross-term survives; the count argument forces each surviving crown pair
to be ({α_t}, {β}).
Sideward Merge case 3(b) realization, F̂ = ∅, unique-witness form.
Corollary of mergeOp_sideward_3b_general_pair when both α and β have
unique matching cuts p_α, p_β.
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, β).
Case 3(a): both accessible terms from the same component #
Sideward Merge case 3(a), F̂ = ∅, multi-witness sum form (M-C-B Lemma 1.4.5, p. 55, eq. (1.3.3)).
mergeOp lbl α_t β on the single-component workspace {T_i} produces a
sum over all 2-edge cuts of T_i whose crown is {α_t, β}.
Sideward Merge case 3(a) realization, F̂ = ∅, unique-witness form.
Corollary of mergeOp_sideward_3a_general_pair when the 2-edge cut
producing {α_t, β} is uniquely witnessed by p0.
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, β).