Size counting on nonplanar rooted trees and workspaces

The MCB size measures for syntactic-object combinatorics ([MCB25]), on the canonical Nonplanar carrier. A workspace (forest) is a Multiset (Nonplanar α); MCB foregrounds the measures b₀/α/σ on workspaces (eq. 1.6.1), with a single tree as the one-component case. The tree-level accCount is the recursive primitive that α folds over.

These build directly on the lifted Nonplanar.numNodes (= MCB's #V); the legacy planar Decorated/AdmissibleCut substrate provided the same measures over the unfaithful planar-binary TraceTree.

Main definitions

• Nonplanar.accCount — accessible-term count α(T) = #V(T) - 1 (tree primitive).
• Forest.b₀ — number of component trees (Betti number).
• Forest.alpha — total accessible terms α(F) = Σ α(Tᵢ).
• Forest.sigma — workspace size σ(F) = b₀(F) + α(F).

Main results

• Nonplanar.accCount_merge — external Merge adds two accessible terms (eq. 1.6.5).
• Forest.sigma_eq_sum_numNodes — σ(F) = #V(F) (eq. 1.2.6); unconditional on the generic carrier (no trace leaves). The contraction-quotient exception (σᶜ ≠ #V, MCB p.66) lives in TraceCounting.

TODO

• Trace-aware accCountC/alphaC/sigmaC and the complexity grading #L on lexical leaves (leafCountSO0) over Nonplanar (α ⊕ β) (TraceCounting.lean); builds on the carrier Nonplanar.numLeaves.
• The admissible-cut layer (Fintype-enumerable cuts + extraction identities 1.6.7/1.6.8).

def RootedTree.Nonplanar.accCount {α : Type u_1} (t : Nonplanar α) : ℕ

The accessible-term count α(T) = #V(T) - 1: every vertex of a syntactic object except its root (MCB eq. 1.2.5).

Equations

• t.accCount = t.numNodes - 1

@[simp]

theorem RootedTree.Nonplanar.accCount_leaf {α : Type u_1} (a : α) : (leaf a).accCount = 0

theorem RootedTree.Nonplanar.accCount_eq_numNodes_sub_one {α : Type u_1} (t : Nonplanar α) : t.accCount = t.numNodes - 1

theorem RootedTree.Nonplanar.accCount_merge {α : Type u_1} (a : α) (l r : Nonplanar α) : (node a {l, r}).accCount = l.accCount + r.accCount + 2

External Merge of two syntactic objects adds exactly two accessible terms (MCB Lemma 1.6.3, eq. 1.6.5).

Workspace (forest) measures

A workspace is a Multiset (Nonplanar α). MCB's primitive workspace measures are b₀ (component count) and α (accessible terms); σ is derived.

def RootedTree.Forest.b₀ {α : Type u_1} (F : Multiset (Nonplanar α)) : ℕ

The number of component trees in a workspace — MCB's b₀, the Betti number b₀(F) = #I (eq. 1.6.1).

Equations

• RootedTree.Forest.b₀ F = F.card

@[simp]

theorem RootedTree.Forest.b₀_zero {α : Type u_1} : b₀ 0 = 0

@[simp]

theorem RootedTree.Forest.b₀_cons {α : Type u_1} (T : Nonplanar α) (F : Multiset (Nonplanar α)) : b₀ (T ::ₘ F) = b₀ F + 1

@[simp]

theorem RootedTree.Forest.b₀_singleton {α : Type u_1} (T : Nonplanar α) : b₀ {T} = 1

@[simp]

theorem RootedTree.Forest.b₀_add {α : Type u_1} (F G : Multiset (Nonplanar α)) : b₀ (F + G) = b₀ F + b₀ G

def RootedTree.Forest.alpha {α : Type u_1} (F : Multiset (Nonplanar α)) : ℕ

Total accessible terms across the workspace, α(F) = Σ α(Tᵢ) (eq. 1.2.4).

Equations

• RootedTree.Forest.alpha F = (Multiset.map RootedTree.Nonplanar.accCount F).sum

@[simp]

theorem RootedTree.Forest.alpha_zero {α : Type u_1} : alpha 0 = 0

@[simp]

theorem RootedTree.Forest.alpha_cons {α : Type u_1} (T : Nonplanar α) (F : Multiset (Nonplanar α)) : alpha (T ::ₘ F) = T.accCount + alpha F

@[simp]

theorem RootedTree.Forest.alpha_singleton {α : Type u_1} (T : Nonplanar α) : alpha {T} = T.accCount

@[simp]

theorem RootedTree.Forest.alpha_add {α : Type u_1} (F G : Multiset (Nonplanar α)) : alpha (F + G) = alpha F + alpha G

def RootedTree.Forest.sigma {α : Type u_1} (F : Multiset (Nonplanar α)) : ℕ

Workspace size σ(F) = b₀(F) + α(F) (MCB eq. 1.6.1): components plus accessible terms. For trace-free workspaces this is the total vertex count (sigma_eq_sum_numNodes); it is not the vertex count for contraction quotients (a trace leaf is a vertex but not an accessible term, MCB p.66).

Equations

• RootedTree.Forest.sigma F = RootedTree.Forest.b₀ F + RootedTree.Forest.alpha F

@[simp]

theorem RootedTree.Forest.sigma_zero {α : Type u_1} : sigma 0 = 0

@[simp]

theorem RootedTree.Forest.sigma_cons {α : Type u_1} (T : Nonplanar α) (F : Multiset (Nonplanar α)) : sigma (T ::ₘ F) = T.numNodes + sigma F

@[simp]

theorem RootedTree.Forest.sigma_add {α : Type u_1} (F G : Multiset (Nonplanar α)) : sigma (F + G) = sigma F + sigma G

theorem RootedTree.Forest.sigma_eq_sum_numNodes {α : Type u_1} (F : Multiset (Nonplanar α)) : sigma F = (Multiset.map Nonplanar.numNodes F).sum

σ(F) = #V(F), the total vertex count (MCB eq. 1.2.6). Unconditional on the generic carrier, where every accCount is numNodes − 1; the contraction-quotient exception lives in TraceCounting.