Trace-aware size counting on Nonplanar (α ⊕ β)

[MCB25]

The MCB size measures specialized to the contraction-quotient carrier Nonplanar (α ⊕ β), where Sum.inl vertices carry original lexical decorations and Sum.inr vertices are trace-marker placeholders left by the Δ^c coproduct (a trace leaf is node (Sum.inr b) [], the encoding of Coproduct.Trace.traceLeaf). A trace leaf is a vertex but not an accessible term: it is excluded from Acc, so the trace-aware counts subtract it off the generic carrier measures.

The key consequence is the failure of the clean trace-free identity σ = #V: for a contraction quotient σᶜ ≠ #V (MCB p. 66 caveat), because a trace leaf inflates #V without contributing an accessible term.

Main definitions

• Nonplanar.traceLeafCount — number of Sum.inr-labeled leaves.
• Nonplanar.accCountC — trace-excluding accessible-term count α − #traceLeaves.
• Nonplanar.leafCountSO0 — complexity grading #L on lexical leaves only.
• Forest.alphaC / Forest.sigmaC — the trace-aware workspace measures.

traceLeafCount — counting trace-marker leaves

A trace marker is a Sum.inr-labeled vertex (always a leaf in practice). A fold over RoseTree (α ⊕ β): at a node, sum the children's counts, adding 1 only for a bare Sum.inr-leaf.

def RoseTree.traceLeafCount {α : Type u_1} {β : Type u_2} : RoseTree (α ⊕ β) → ℕ

The number of Sum.inr-labeled leaves (trace markers) in a tree.

Equations

• RoseTree.traceLeafCount = RoseTree.fold fun (v : α ⊕ β) (ns : List ℕ) => match v, ns with | Sum.inr val, [] => 1 | x, ns => ns.sum

@[simp]

theorem RoseTree.traceLeafCount_leaf_inr {α : Type u_1} {β : Type u_2} (b : β) : (node (Sum.inr b) []).traceLeafCount = 1

@[simp]

theorem RoseTree.traceLeafCount_leaf_inl {α : Type u_1} {β : Type u_2} (a : α) : (node (Sum.inl a) []).traceLeafCount = 0

theorem RoseTree.traceLeafCount_node_of_ne_nil {α : Type u_1} {β : Type u_2} (v : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) (h : cs ≠ []) : (node v cs).traceLeafCount = (List.map traceLeafCount cs).sum

On a non-leaf node, traceLeafCount is the sum of the children's counts, regardless of the root label's Sum-side. Clears the empty/nonempty split.

@[simp]

theorem RoseTree.traceLeafCount_node_inl {α : Type u_1} {β : Type u_2} (a : α) (cs : List (RoseTree (α ⊕ β))) : (node (Sum.inl a) cs).traceLeafCount = (List.map traceLeafCount cs).sum

On a Sum.inl root the count is just the children's total (the lexical root is never itself a trace leaf), for any child list.

Trace-leaf-count invariance under PermEquiv

theorem RoseTree.traceLeafCount_permEquiv {α : Type u_1} {β : Type u_2} {t s : RoseTree (α ⊕ β)} (h : t.PermEquiv s) : t.traceLeafCount = s.traceLeafCount

traceDepthSum — depth-weighted trace-marker count (Minimal Search depth)

The Minimal Search depth d_v of MCB §1.5.2 (book p. 59): the sum over trace-marker leaves of their distance from the root. Descending into the children adds 1 per trace leaf below them (+ (cs.map traceLeafCount).sum), so a trace leaf at depth d is counted d times, contributing d. A bare trace leaf at the root contributes 0.

The recurrence couples to traceLeafCount at each level, so a single fold does not express it; it is structural recursion with a child-list companion.

For a Δ^c cut, the quotient (trunk) places a trace leaf at each cut site at exactly the cut depth (Coproduct.Trace.traceLeaf), so traceDepthSum(quotient) reads off the total extraction depth Σ d_{v_i} of MCB rule 1 directly — no enumeration tagging required.

def RoseTree.traceDepthSum {α : Type u_1} {β : Type u_2} : RoseTree (α ⊕ β) → ℕ

Sum of root-distances of the Sum.inr-labeled (trace-marker) leaves.

Equations

• (RoseTree.node value cs).traceDepthSum = RoseTree.traceDepthSumList cs + (List.map RoseTree.traceLeafCount cs).sum

def RoseTree.traceDepthSumList {α : Type u_1} {β : Type u_2} : List (RoseTree (α ⊕ β)) → ℕ

Auxiliary: trace-depth across a list of children, measured in the children's own frame (the parent adds the +1-per-level offset).

Equations

• RoseTree.traceDepthSumList [] = 0
• RoseTree.traceDepthSumList (t :: ts) = t.traceDepthSum + RoseTree.traceDepthSumList ts

theorem RoseTree.traceDepthSum_node {α : Type u_1} {β : Type u_2} (v : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) : (node v cs).traceDepthSum = traceDepthSumList cs + (List.map traceLeafCount cs).sum

@[simp]

theorem RoseTree.traceDepthSumList_nil {α : Type u_1} {β : Type u_2} : traceDepthSumList [] = 0

@[simp]

theorem RoseTree.traceDepthSumList_cons {α : Type u_1} {β : Type u_2} (t : RoseTree (α ⊕ β)) (ts : List (RoseTree (α ⊕ β))) : traceDepthSumList (t :: ts) = t.traceDepthSum + traceDepthSumList ts

@[simp]

theorem RoseTree.traceDepthSum_leaf_inl {α : Type u_1} {β : Type u_2} (a : α) : (node (Sum.inl a) []).traceDepthSum = 0

@[simp]

theorem RoseTree.traceDepthSum_leaf_inr {α : Type u_1} {β : Type u_2} (b : β) : (node (Sum.inr b) []).traceDepthSum = 0

theorem RoseTree.traceDepthSumList_eq_sum_map {α : Type u_1} {β : Type u_2} (cs : List (RoseTree (α ⊕ β))) : traceDepthSumList cs = (List.map traceDepthSum cs).sum

theorem RoseTree.traceDepthSum_node_eq {α : Type u_1} {β : Type u_2} (v : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) : (node v cs).traceDepthSum = (List.map (fun (c : RoseTree (α ⊕ β)) => c.traceDepthSum + c.traceLeafCount) cs).sum

The per-child contribution traceDepthSum c + traceLeafCount c summed: combines the two child statistics into one map.

Trace-depth invariance under PermEquiv

theorem RoseTree.traceDepthSum_permEquiv {α : Type u_1} {β : Type u_2} {t s : RoseTree (α ⊕ β)} (h : t.PermEquiv s) : t.traceDepthSum = s.traceDepthSum

theorem RoseTree.traceLeafCount_le_node {α : Type u_1} {β : Type u_2} (v : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) : (List.map traceLeafCount cs).sum ≤ (node v cs).traceLeafCount

The children's trace leaves are bounded by the node's: a Sum.inr root can only add a trace leaf (the empty-trace-leaf case), never remove one.

theorem RoseTree.traceLeafCount_le_traceDepthSum_of_inl {α : Type u_1} {β : Type u_2} (a : α) (cs : List (RoseTree (α ⊕ β))) : (node (Sum.inl a) cs).traceLeafCount ≤ (node (Sum.inl a) cs).traceDepthSum

A lexical root puts every trace marker at depth ≥ 1: for a Sum.inl-rooted tree, the depth-weighted trace count dominates the plain trace count. Underlies the Minimal-Search positivity Cut.depthC_pos.

def RootedTree.Nonplanar.traceLeafCount {α : Type u_1} {β : Type u_2} : Nonplanar (α ⊕ β) → ℕ

The number of Sum.inr-labeled (trace-marker) leaves of a nonplanar tree, lifted from RoseTree.traceLeafCount.

Equations

• RootedTree.Nonplanar.traceLeafCount = RootedTree.Nonplanar.lift RoseTree.traceLeafCount ⋯

@[simp]

theorem RootedTree.Nonplanar.traceLeafCount_mk {α : Type u_1} {β : Type u_2} (t : RoseTree (α ⊕ β)) : (mk t).traceLeafCount = t.traceLeafCount

@[simp]

theorem RootedTree.Nonplanar.traceLeafCount_leaf_inl {α : Type u_1} {β : Type u_2} (a : α) : (leaf (Sum.inl a)).traceLeafCount = 0

@[simp]

theorem RootedTree.Nonplanar.traceLeafCount_leaf_inr {α : Type u_1} {β : Type u_2} (b : β) : (leaf (Sum.inr b)).traceLeafCount = 1

def RootedTree.Nonplanar.traceDepthSum {α : Type u_1} {β : Type u_2} : Nonplanar (α ⊕ β) → ℕ

The Minimal Search depth d_v of MCB §1.5: the sum of root-distances of the trace-marker leaves, lifted from RoseTree.traceDepthSum. For a Δ^c cut, traceDepthSum of the quotient is the total extraction depth.

Equations

• RootedTree.Nonplanar.traceDepthSum = RootedTree.Nonplanar.lift RoseTree.traceDepthSum ⋯

@[simp]

theorem RootedTree.Nonplanar.traceDepthSum_mk {α : Type u_1} {β : Type u_2} (t : RoseTree (α ⊕ β)) : (mk t).traceDepthSum = t.traceDepthSum

@[simp]

theorem RootedTree.Nonplanar.traceDepthSum_leaf_inl {α : Type u_1} {β : Type u_2} (a : α) : (leaf (Sum.inl a)).traceDepthSum = 0

@[simp]

theorem RootedTree.Nonplanar.traceDepthSum_leaf_inr {α : Type u_1} {β : Type u_2} (b : β) : (leaf (Sum.inr b)).traceDepthSum = 0

@[simp]

theorem RootedTree.Nonplanar.traceDepthSum_node_inl {α : Type u_1} {β : Type u_2} (a : α) (F : Multiset (Nonplanar (α ⊕ β))) : (node (Sum.inl a) F).traceDepthSum = (Multiset.map (fun (c : Nonplanar (α ⊕ β)) => c.traceDepthSum + c.traceLeafCount) F).sum

Trace-depth of a node decomposes over children: each child c contributes its own trace-depth plus one per trace leaf it carries (the +1 for the extra level between the node and c).

def RootedTree.Nonplanar.accCountC {α : Type u_1} {β : Type u_2} (t : Nonplanar (α ⊕ β)) : ℕ

The trace-excluding accessible-term count αᶜ(T) = α(T) − #traceLeaves(T): a trace leaf is a vertex but not an accessible term (MCB p. 66). Truncated subtraction handles the all-trace edge case (e.g. T = traceLeaf b, where α = 0 and #traceLeaves = 1).

Equations

• t.accCountC = t.accCount - t.traceLeafCount

@[simp]

theorem RootedTree.Nonplanar.traceLeafCount_node_inl {α : Type u_1} {β : Type u_2} (a : α) (F : Multiset (Nonplanar (α ⊕ β))) : (node (Sum.inl a) F).traceLeafCount = (Multiset.map traceLeafCount F).sum

Trace leaves of a lexical-rooted node: the root contributes none, so the count is the children's total.

theorem RootedTree.Nonplanar.accCountC_merge {α : Type u_1} {β : Type u_2} (a : α) (l r : Nonplanar (α ⊕ β)) (hl : l.traceLeafCount < l.numNodes) (hr : r.traceLeafCount < r.numNodes) : (node (Sum.inl a) {l, r}).accCountC = l.accCountC + r.accCountC + 2

External Merge adds two accessible terms in the trace-aware count: the two children's roots become accessible (MCB Lemma 1.6.3, eq. 1.6.5). Needs each child to have a lexical vertex (traceLeafCount < numNodes), automatic for a real syntactic object.

def RootedTree.Nonplanar.leafCountSO0 {α : Type u_1} {β : Type u_2} (t : Nonplanar (α ⊕ β)) : ℕ

The complexity grading #L restricted to lexical leaves: #L_{SO₀}(T) = #L(T) − #traceLeaves(T). The trace-exclusion follows the UNVERIFIED-default reading of MCB Remark 1.2.2 (leaves labeled by SO₀); whether a trace leaf counts in #L is not settled in the book.

Equations

• t.leafCountSO0 = t.numLeaves - t.traceLeafCount

Trace-aware workspace (forest) measures

def RootedTree.Forest.alphaC {α : Type u_1} {β : Type u_2} (F : Multiset (Nonplanar (α ⊕ β))) : ℕ

Trace-excluding accessible terms across a workspace, αᶜ(F) = Σ αᶜ(Tᵢ).

Equations

• RootedTree.Forest.alphaC F = (Multiset.map RootedTree.Nonplanar.accCountC F).sum

@[simp]

theorem RootedTree.Forest.alphaC_zero {α : Type u_1} {β : Type u_2} : alphaC 0 = 0

@[simp]

theorem RootedTree.Forest.alphaC_cons {α : Type u_1} {β : Type u_2} (T : Nonplanar (α ⊕ β)) (F : Multiset (Nonplanar (α ⊕ β))) : alphaC (T ::ₘ F) = T.accCountC + alphaC F

@[simp]

theorem RootedTree.Forest.alphaC_singleton {α : Type u_1} {β : Type u_2} (T : Nonplanar (α ⊕ β)) : alphaC {T} = T.accCountC

@[simp]

theorem RootedTree.Forest.alphaC_add {α : Type u_1} {β : Type u_2} (F G : Multiset (Nonplanar (α ⊕ β))) : alphaC (F + G) = alphaC F + alphaC G

def RootedTree.Forest.sigmaC {α : Type u_1} {β : Type u_2} (F : Multiset (Nonplanar (α ⊕ β))) : ℕ

Trace-aware workspace size σᶜ(F) = b₀(F) + αᶜ(F). Unlike the generic σ, this is not the vertex count for contraction quotients (σᶜ ≠ #V, MCB p. 66): a trace leaf is a vertex but not an accessible term, so it raises #V without raising σᶜ.

Equations

• RootedTree.Forest.sigmaC F = RootedTree.Forest.b₀ F + RootedTree.Forest.alphaC F

@[simp]

theorem RootedTree.Forest.sigmaC_zero {α : Type u_1} {β : Type u_2} : sigmaC 0 = 0

@[simp]

theorem RootedTree.Forest.sigmaC_cons {α : Type u_1} {β : Type u_2} (T : Nonplanar (α ⊕ β)) (F : Multiset (Nonplanar (α ⊕ β))) : sigmaC (T ::ₘ F) = T.accCountC + 1 + sigmaC F

@[simp]

theorem RootedTree.Forest.sigmaC_add {α : Type u_1} {β : Type u_2} (F G : Multiset (Nonplanar (α ⊕ β))) : sigmaC (F + G) = sigmaC F + sigmaC G

The σᶜ ≠ #V caveat, concretely

A lexical root over a single trace leaf: #V = 2 (root + trace leaf) but the trace leaf contributes no accessible term, so αᶜ = 0 and σᶜ = 1.