No Complexity Loss (NCL) for algebraic Merge #
[MCB25] Proposition 1.6.10, book p. 72.
Implements M-C-B Definition 1.6.2 (book p. 64) and Proposition 1.6.10
(book p. 72) on the canonical carrier: a workspace transformation
F → F' (over Forest (Nonplanar α)) satisfies No Complexity Loss if
some component map Φ₀ is nondecreasing in degree.
Grading choice: vertex count #
M-C-B grade by leaf count #L. We grade by Nonplanar.numNodes (vertex
count) — the canonical Connes–Kreimer grading. The deletion coproduct
conserves weight exactly (cutSummandsN_numNodes) for every cut, with
none of the nullary-node corrections that leaf count incurs when a node
loses all its children under a multi-edge cut. NCL is a nondecreasing
condition, and weight delivers every conclusion leaf count would: the
Merge node's weight strictly exceeds each operand's (numNodes_node adds
the root), and every deletion quotient's weight is strictly smaller than
its source (a nonempty crown carries positive weight). So the
weight-graded NCL is both cleaner and strictly-more-robust than a
leaf-count port.
Contents #
NCLBetween F F': existential form — some component map is weight-nondecreasing.em_case1_satisfiesNCL: EM Case 1{S, S'} + F̂ → {M(S,S')} + F̂viaS, S' ↦ M(S,S'), spectators fixed.im_satisfiesNCL: IM{T} → {M(Q, β)}(Q = T/β via a single-edge cut) via the constant map; weight follows fromcutSummandsN_numNodes.InducedMapNCL/DLPerComponent: MCB Def 1.6.2 strict form + the per-component degree-loss function (eq. 1.6.4).sideward_{2b,3a,3b}_violatesInducedMapNCL: under the canonical induced map, each Sideward configuration fails NCL — the deletion quotient is strictly lighter than its source.
M-C-B Definition 1.6.2 (book p. 64), existential form. A workspace
transformation F → F' satisfies No Complexity Loss if some component
map Φ₀ lands in F' and never decreases weight (the vertex-count
Hopf grading; see the module docstring on the grading choice).
Equations
- One or more equations did not get rendered due to their size.
Instances For
M-C-B Prop 1.6.10, EM Case-1 direction. The EM workspace equation
carries a component map satisfying NCL: S, S' ↦ M(S, S') (weight
increases by 1 + the other operand's weight); each T ∈ F̂ ↦ itself
(weight preserved).
Quoting M-C-B (book p. 72): "deg(𝔐(T_i, T_j)) = deg(T_i) + deg(T_j), which is greater than or equal to both deg(T_i) and deg(T_j). All the remaining components of the workspace not used by Merge maintain the same degree."
M-C-B Prop 1.6.10, IM positive direction. The IM workspace
transformation {T} → {M(Q, β)} (Q = T/β the deletion-quotient of the
single-edge cut p0 extracting β) carries the constant component map
T ↦ M(Q, β), with (M(Q, β)).numNodes = 1 + Q.numNodes + β.numNodes = 1 + T.numNodes ≥ T.numNodes by cutSummandsN_numNodes.
Quoting M-C-B (book p. 72): "For Internal Merge, similarly, deg(T_v, T/T_v) = deg(T)." (Under the weight grading the Merge node adds its own vertex, so the inequality is strict; NCL holds a fortiori.)
No T ≠ β hypothesis is required (cf. mergeOp_im_composition, which
needs it for non-degeneracy of the algebraic sum, not for NCL).
InducedMapNCL — MCB Def 1.6.2 with the canonical map #
MCB Definition 1.6.2 (book p. 64), strict form. The canonical
induced map Φ_0 : π_0(F) → π_0(Φ(F)) is named explicitly. NCL holds
iff every component T ∈ F has (Φ_0 T).numNodes ≥ T.numNodes.
Compare NCLBetween (existential: "some map works"). The strict form
is needed for the negative direction: a Sideward operation might satisfy
NCLBetween via some non-canonical map, but its canonical map (each
root to where its image lives) fails.
Equations
- Minimalist.Merge.InducedMapNCL F F' Φ_0 = ((∀ (T : RootedTree.Nonplanar α) (h : T ∈ F), Φ_0 T h ∈ F') ∧ ∀ (T : RootedTree.Nonplanar α) (h : T ∈ F), (Φ_0 T h).numNodes ≥ T.numNodes)
Instances For
Strict form ⇒ existential form.
MCB eq. 1.6.4 — per-component degree-loss function. Per-component
weight difference; NCL ⇔ all values ≥ 0 (matches InducedMapNCL.2).
Int-valued so violations surface as negative numbers rather than being
clamped by ℕ-subtraction.
Equations
- Minimalist.Merge.DLPerComponent Φ_0 T h = ↑(Φ_0 T h).numNodes - ↑T.numNodes
Instances For
NCL inequality (eq. 1.6.3) per component restated via DLPerComponent.
Sideward NCL negative direction (MCB Prop 1.6.10) #
MCB Prop 1.6.10 negative — Sideward 2(b) violates InducedMapNCL.
Under the canonical induced map, {T_i, T_j} → {M(T_i, β), T_j/β}
fails NCL because T_j ↦ T_j/β = T_j_q strictly drops weight.
MCB (book p. 72): "the root of the component T is mapped … to the root of the component T/T_v in the new workspace F', with deg(T/T_v) < deg(T); thus, it violates the No Complexity Loss constraint."
MCB Prop 1.6.10 negative — Sideward 3(a) violates InducedMapNCL.
Workspace {T_i} → {M(a, b), T_i/(a⊔b)} for a 2-edge cut on T_i
extracting both a and b. The canonical map sends T_i ↦ T_i/(a⊔b),
which has lost both subtrees, so its weight is strictly smaller. (Weight
conservation is exact here even though leaf count would not be —
cutSummandsN_numNodes holds for the 2-edge crown directly.)
MCB Prop 1.6.10 negative — Sideward 3(b) violates InducedMapNCL.
Workspace {T_i, T_j} → {M(a, b), T_i/a, T_j/b}. The canonical map
sends T_i ↦ T_i/a (and T_j ↦ T_j/b); the T_i/a = T_iq component
strictly drops weight, so NCL fails already at T_i.