No Complexity Loss

No Complexity Loss is a condition on a transformation F → F' of workspaces: some map sending each component of F to a component of F' is nondecreasing in degree, so Merge builds hierarchical structure of nondecreasing complexity. NoComplexityLoss F F' is the existential form and NoComplexityLoss.Map F F' Φ₀ the form for a given component map, with NoComplexityLoss.degreeLoss the per-component degree difference whose nonnegativity it asserts.

On the shapes the cases of Merge produce, External and Internal Merge satisfy the condition, and each Sideward configuration fails it under its canonical component map, because a deletion quotient is strictly lighter than its source.

Implementation notes

The book grades by leaf count. We grade by UnorderedTree.numNodes, the canonical Connes–Kreimer grading: the deletion coproduct conserves it exactly (cutSummandsN_numNodes) for every cut, with none of the nullary-node corrections leaf count incurs when a node loses all its children under a multi-edge cut. The condition is a nondecreasing one, and vertex count delivers every conclusion leaf count would: the Merge node's weight strictly exceeds each operand's, and every deletion quotient's weight is strictly smaller than its source.

Main definitions

• Minimalist.NoComplexityLoss, Minimalist.NoComplexityLoss.Map
• Minimalist.NoComplexityLoss.degreeLoss: the per-component degree-loss function.

Main results

• Minimalist.NoComplexityLoss.em_case1, NoComplexityLoss.im: External and Internal Merge satisfy the condition.
• Minimalist.NoComplexityLoss.not_map_sideward_2b, _3a, _3b: the Sideward configurations fail it under the canonical map.

References

• [marcolli-chomsky-berwick-2025], §1.6.1 and §1.6.3 (Definition 1.6.2, Proposition 1.6.10)

def Minimalist.NoComplexityLoss {α : Type u_1} (F F' : UnorderedTree.Forest (UnorderedTree α)) : 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 Φ₀ 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.

theorem Minimalist.NoComplexityLoss.em_case1 {α : Type u_1} [DecidableEq (UnorderedTree α)] (lbl : α) (S S' : UnorderedTree α) (Fhat : UnorderedTree.Forest (UnorderedTree α)) : NoComplexityLoss ({S, S'} + Fhat) ({UnorderedTree.node lbl {S, S'}} + Fhat)

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."

theorem Minimalist.NoComplexityLoss.im {α : Type u_1} (lbl : α) (β T Q : UnorderedTree α) (p0 : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (hp0 : p0 ∈ ConnesKreimer.cutSummandsN T) (h_cf : p0.1 = {β}) (h_remainder : p0.2 = Q) : NoComplexityLoss {T} {UnorderedTree.node lbl {Q, β}}

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).

NoComplexityLoss.Map — MCB Def 1.6.2 with the canonical map

def Minimalist.NoComplexityLoss.Map {α : Type u_1} (F F' : UnorderedTree.Forest (UnorderedTree α)) (Φ_0 : (T : UnorderedTree α) → T ∈ F → UnorderedTree α) : 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 every component T ∈ F has (Φ_0 T).numNodes ≥ T.numNodes.

Compare NoComplexityLoss (existential: "some map works"). The strict form is needed for the negative direction: a Sideward operation might satisfy NoComplexityLoss via some non-canonical map, but its canonical map (each root to where its image lives) fails.

Equations

• Minimalist.NoComplexityLoss.Map F F' Φ_0 = ((∀ (T : UnorderedTree α) (h : T ∈ F), Φ_0 T h ∈ F') ∧ ∀ (T : UnorderedTree α) (h : T ∈ F), (Φ_0 T h).numNodes ≥ T.numNodes)

theorem Minimalist.NoComplexityLoss.of_map {α : Type u_1} {F F' : UnorderedTree.Forest (UnorderedTree α)} {Φ_0 : (T : UnorderedTree α) → T ∈ F → UnorderedTree α} (h : Map F F' Φ_0) : NoComplexityLoss F F'

Strict form ⇒ existential form.

def Minimalist.NoComplexityLoss.degreeLoss {α : Type u_1} {F : UnorderedTree.Forest (UnorderedTree α)} (Φ_0 : (T : UnorderedTree α) → T ∈ F → UnorderedTree α) (T : UnorderedTree α) (h : T ∈ F) : ℤ

MCB eq. 1.6.4 — per-component degree-loss function. Per-component weight difference; NCL ⇔ all values ≥ 0 (matches NoComplexityLoss.Map.2). Int-valued so violations surface as negative numbers rather than being clamped by ℕ-subtraction.

Equations

• Minimalist.NoComplexityLoss.degreeLoss Φ_0 T h = ↑(Φ_0 T h).numNodes - ↑T.numNodes

theorem Minimalist.NoComplexityLoss.map_iff_degreeLoss_nonneg {α : Type u_1} {F F' : UnorderedTree.Forest (UnorderedTree α)} (Φ_0 : (T : UnorderedTree α) → T ∈ F → UnorderedTree α) (h_image : ∀ (T : UnorderedTree α) (h : T ∈ F), Φ_0 T h ∈ F') : Map F F' Φ_0 ↔ ∀ (T : UnorderedTree α) (h : T ∈ F), degreeLoss Φ_0 T h ≥ 0

NCL inequality (eq. 1.6.3) per component restated via NoComplexityLoss.degreeLoss.

Sideward NCL negative direction (MCB Prop 1.6.10)

theorem Minimalist.NoComplexityLoss.not_map_sideward_2b {α : Type u_1} [DecidableEq (UnorderedTree α)] (lbl : α) (T_i T_j β T_j_q : UnorderedTree α) (p_j : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (hp_j : p_j ∈ ConnesKreimer.cutSummandsN T_j) (h_cf : p_j.1 = {β}) (h_rd : p_j.2 = T_j_q) (h_distinct : T_i ≠ T_j) : ¬Map {T_i, T_j} {UnorderedTree.node lbl {T_i, β}, T_j_q} fun (T : UnorderedTree α) (x : T ∈ {T_i, T_j}) => if T = T_i then UnorderedTree.node lbl {T_i, β} else T_j_q

MCB Prop 1.6.10 negative — Sideward 2(b) violates NoComplexityLoss.Map. 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."

theorem Minimalist.NoComplexityLoss.not_map_sideward_3a {α : Type u_1} (lbl : α) (T_i a b T_iq : UnorderedTree α) (p_i : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (hp_i : p_i ∈ ConnesKreimer.cutSummandsN T_i) (h_cf : p_i.1 = {a, b}) (h_rd : p_i.2 = T_iq) : ¬Map {T_i} {UnorderedTree.node lbl {a, b}, T_iq} fun (x : UnorderedTree α) (x_1 : x ∈ {T_i}) => T_iq

MCB Prop 1.6.10 negative — Sideward 3(a) violates NoComplexityLoss.Map. 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.)

theorem Minimalist.NoComplexityLoss.not_map_sideward_3b {α : Type u_1} [DecidableEq (UnorderedTree α)] (lbl : α) (T_i T_j a b T_iq T_jq : UnorderedTree α) (p_i : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α) (hp_i : p_i ∈ ConnesKreimer.cutSummandsN T_i) (h_cf_i : p_i.1 = {a}) (h_rd_i : p_i.2 = T_iq) : ¬Map {T_i, T_j} {UnorderedTree.node lbl {a, b}, T_iq, T_jq} fun (T : UnorderedTree α) (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 NoComplexityLoss.Map. 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.