No Complexity Loss (NCL) for algebraic Merge

@cite{marcolli-chomsky-berwick-2025} 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): a workspace transformation F → F' satisfies No Complexity Loss if some component map Φ₀ from F to F' is nondecreasing in leafCount (the algebraic analog of MCB's "degree").

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. For Internal Merge, similarly, deg(T_v, T/T_v) = deg(T)."

Contents

• NCLBetween F F': existential form of NCL — there exists a component map satisfying the nondecreasing-leafCount condition.
• em_case1_satisfiesNCL: the EM Case-1 transformation {S, S'} + F̂ → {.node S S'} + F̂ satisfies NCL via the map S, S' ↦ .node S S'; each spectator maps to itself.
• im_satisfiesNCL: the IM transformation {T} → {.node Q β} (where Q = T/β via cut c0) satisfies NCL via the constant map; the leafCount equality follows from CutShape.cut_leafCount_conservation (the Δ^d analog of MCB's degree-conservation remark).

Status

Both EM Case-1 and IM positive directions sorry-free.

InducedMapNCL: MCB Def 1.6.2 verbatim form

NCLBetween is the existential form (some map works). MCB Def 1.6.2 demands the canonical induced map Φ_0 : π_0(F) → π_0(Φ(F)) satisfies the inequality — Φ_0 is determined by Φ (it sends each root to the component containing its image).

InducedMapNCL F F' Φ_0 exposes the induced map as an explicit parameter rather than existentially quantifying it. This is needed for the NEGATIVE direction (Sideward 2(b)/3(a)/3(b) violate NCL) — under the existential form NCLBetween, one could falsely satisfy NCL by choosing a non-canonical map; the strict form forces the canonical map.

DL: degree-loss function (MCB eq. 1.6.4)

DL Φ_0 F = min_{a ∈ π_0(F)} (deg(Φ_0(a)) - deg(a)). NCL ⇔ DL ≥ 0. Implemented as DLValue returning Int (so we can express negative values without ℕ-subtraction issues).

Sideward NCL negative direction (Prop 1.6.10 negative)

sideward_2b_violatesInducedMapNCL, sideward_3a_violatesInducedMapNCL, sideward_3b_violatesInducedMapNCL: under the canonical induced map that sends each original root to the component containing its image, Sideward operations fail NCL because the deletion-quotient (T/T_v) has strictly smaller leafCount than T.

Architectural note

NCL is a predicate about Merge transformations, not a Merge operation itself. It sits at the bottom of the Merge dependency chain (consumes both External and Internal). When Sideward NCL lands, this file will import Sideward.lean too.

def Minimalist.Merge.NCLBetween {α : Type u_1} [DecidableEq α] (F F' : ConnesKreimer.TraceForest α Unit) : Prop

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 Φ₀ : ∀ T ∈ F, TraceTree α Unit lands in F' and never decreases leafCount. The Hopf grading deg(a) = #L(T_a) is TraceTree.leafCount (M-C-B identifies these on book p. 64).

See the section docstring for the relationship to M-C-B's induced component map (a strengthening this version doesn't enforce).

Equations

• One or more equations did not get rendered due to their size.

theorem Minimalist.Merge.em_case1_satisfiesNCL {α : Type u_1} [DecidableEq α] (S S' : ConnesKreimer.TraceTree α Unit) (Fhat : ConnesKreimer.TraceForest α Unit) : NCLBetween ({S, S'} + Fhat) ({S.node S'} + Fhat)

M-C-B Prop 1.6.10, EM Case-1 direction. The EM workspace equation proved by mergeOp_eps_zero_residual carries a component map satisfying NCL: S, S' ↦ .node S S' (degree increases by the other operand's positive leafCount); each T ∈ F̂ ↦ itself (degree 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."

theorem Minimalist.Merge.im_satisfiesNCL {α : Type u_1} [DecidableEq α] (β T Q : ConnesKreimer.TraceTree α Unit) (c0 : ConnesKreimer.CutShape T) (h_cf : c0.cutForest = {β}) (h_remainder : c0.remainderDeletion = some Q) : NCLBetween {T} {Q.node β}

M-C-B Prop 1.6.10, IM positive direction. The IM workspace transformation {T} → {.node Q β} (where Q = T/β is the deletion- quotient via the unique cut c0 extracting β) carries a component map satisfying NCL: T ↦ .node Q β, with (.node Q β).leafCount = T.leafCount by leafCount conservation under Δ^d (cut_leafCount_conservation, the Δ^d analog of M-C-B's degree-conservation remark, book p. 64 — paragraph after Def 1.6.2).

Quoting M-C-B (book p. 72): "For Internal Merge, similarly, deg(T_v, T/T_v) = deg(T)."

The substrate hypotheses match the ones for mergeOp_im_composition: c0 is the unique cut with cutForest = {β} and remainderDeletion = some Q.

Note: no T ≠ β hypothesis is required (cf. mergeOp_im_composition which does require it for non-degeneracy of the algebraic sum). For NCL the diagonal case is fine — the component map sends T ↦ .node Q β with leafCount equality holding regardless.

§2: InducedMapNCL — MCB Def 1.6.2 verbatim with canonical map

def Minimalist.Merge.InducedMapNCL {α : Type u_1} [DecidableEq α] (F F' : ConnesKreimer.TraceForest α Unit) (Φ_0 : (T : ConnesKreimer.TraceTree α Unit) → T ∈ F → ConnesKreimer.TraceTree α Unit) : Prop

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 for all components T ∈ F, (Φ_0 T).leafCount ≥ T.leafCount.

Compare to NCLBetween: that's existential ("some map works"); this one fixes the map. NCLBetween F F' = ∃ Φ_0, InducedMapNCL F F' Φ_0 (with image-in-F' constraint).

Required for the NEGATIVE direction (sideward_*_violatesInducedMapNCL): a Sideward operation might satisfy NCLBetween via some non-canonical map, but its CANONICAL map (sending each root to where its image lives) fails.

Equations

• One or more equations did not get rendered due to their size.

theorem Minimalist.Merge.NCLBetween_of_InducedMapNCL {α : Type u_1} [DecidableEq α] {F F' : ConnesKreimer.TraceForest α Unit} {Φ_0 : (T : ConnesKreimer.TraceTree α Unit) → T ∈ F → ConnesKreimer.TraceTree α Unit} (h : InducedMapNCL F F' Φ_0) : NCLBetween F F'

Strict form ⇒ existential form: from a canonical induced map satisfying NCL, the existential NCLBetween follows.

def Minimalist.Merge.DLPerComponent {α : Type u_1} [DecidableEq α] {F : ConnesKreimer.TraceForest α Unit} (Φ_0 : (T : ConnesKreimer.TraceTree α Unit) → T ∈ F → ConnesKreimer.TraceTree α Unit) (T : ConnesKreimer.TraceTree α Unit) (h : T ∈ F) : ℤ

MCB eq. 1.6.4 — per-component degree-loss function. Per-component leafCount difference. NCL ⇔ all values ≥ 0 (matches InducedMapNCL.2).

Int rather than ℕ so that violations show up as negative values rather than being clamped to 0 by ℕ-subtraction.

Equations

• Minimalist.Merge.DLPerComponent Φ_0 T h = ↑(Φ_0 T h).leafCount - ↑T.leafCount

theorem Minimalist.Merge.DLPerComponent_nonneg_iff_NCL {α : Type u_1} [DecidableEq α] {F F' : ConnesKreimer.TraceForest α Unit} (Φ_0 : (T : ConnesKreimer.TraceTree α Unit) → T ∈ F → ConnesKreimer.TraceTree α Unit) (h_image : ∀ (T : ConnesKreimer.TraceTree α Unit) (h : T ∈ F), Φ_0 T h ∈ F') : InducedMapNCL F F' Φ_0 ↔ ∀ (T : ConnesKreimer.TraceTree α Unit) (h : T ∈ F), DLPerComponent Φ_0 T h ≥ 0

NCL inequality (eq. 1.6.3) per component restated via DLPerComponent.

§3: Sideward NCL negative direction (MCB Prop 1.6.10)

theorem Minimalist.Merge.sideward_2b_violatesInducedMapNCL {α : Type u_1} [DecidableEq α] (T_i T_j β T_j_q : ConnesKreimer.TraceTree α Unit) (c_j : ConnesKreimer.CutShape T_j) (h_cf : c_j.cutForest = {β}) (h_rd : c_j.remainderDeletion = some T_j_q) (h_distinct : T_i ≠ T_j) : ¬InducedMapNCL {T_i, T_j} {T_i.node β, T_j_q} fun (T : ConnesKreimer.TraceTree α Unit) (x : T ∈ {T_i, T_j}) => if T = T_i then T_i.node β else T_j_q

MCB Prop 1.6.10 negative — Sideward 2(b) violates InducedMapNCL. Under the canonical induced map sending each root to the component containing its image, Sideward 2(b) {T_i, T_j} → {.node T_i β, T_j/β} fails NCL because T_j ↦ T_j/β has strictly smaller leafCount.

MCB (book p. 72): "the root of the component T is mapped (as in Definition 1.6.2) 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."

For the canonical map specifically: Φ_0(T_i) = .node T_i β, Φ_0(T_j) = T_j/β = T_j_q. The latter has leafCount strictly less than T_j (since β.leafCount ≥ 1 and conservation gives T_j.leafCount = β.leafCount + T_j_q.leafCount).

theorem Minimalist.Merge.sideward_3a_violatesInducedMapNCL {α : Type u_1} [DecidableEq α] (T_i a b T_iq : ConnesKreimer.TraceTree α Unit) (c_i : ConnesKreimer.CutShape T_i) (h_cf : c_i.cutForest = {a, b}) (h_rd : c_i.remainderDeletion = some T_iq) : ¬InducedMapNCL {T_i} {a.node b, T_iq} fun (x : ConnesKreimer.TraceTree α Unit) (x_1 : x ∈ {T_i}) => T_iq

MCB Prop 1.6.10 negative — Sideward 3(a) violates InducedMapNCL. Workspace {T_i} → {.node a b, T_i/(a⊔b)} for a 2-edge cut on T_i extracting both a and b. Canonical map sends T_i ↦ T_i/(a⊔b) (the deletion-quotient component containing T_i's root image). Since the quotient has lost both a and b, its leafCount is strictly less than T_i's.

theorem Minimalist.Merge.sideward_3b_violatesInducedMapNCL {α : Type u_1} [DecidableEq α] (T_i T_j a b T_iq T_jq : ConnesKreimer.TraceTree α Unit) (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) (_h_distinct : T_i ≠ T_j) : ¬InducedMapNCL {T_i, T_j} {a.node b, T_iq, T_jq} fun (T : ConnesKreimer.TraceTree α Unit) (x : T ∈ {T_i, T_j}) => if T = T_i then T_iq else T_jq

MCB Prop 1.6.10 negative — Sideward 3(b) violates InducedMapNCL. Workspace {T_i, T_j} → {.node a b, T_i/a, T_j/b}. Canonical map sends T_i ↦ T_i/a and T_j ↦ T_j/b (each root maps to its deletion-quotient component). Both quotients have strictly smaller leafCount, so NCL fails.