Trace vocabulary for the leaf statistics

[MCB25]

MCB's vocabulary over the generic measures of Counting.lean: the letter names (accCount for numEdges; b₀, alpha, sigma for the forest measures), the p-discounted measures (accCountP, alphaP, sigmaP), and their instantiations at the trace-marker color class Sum.isRight (traceLeafCount, traceDepthSum, accCountC, alphaC, sigmaC).

Domain vocabulary over the generic substrate of Core/Data/RoseTree/Count.lean; consumed by the workspace conservation laws (Workspace/Conservation.lean) and the Merge economy files.

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

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

Equations

• t.traceLeafCount = RoseTree.leafCountP (fun (x : α ⊕ β) => x.isRight = true) t

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

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

Equations

• t.traceDepthSum = RoseTree.leafDepthSumP (fun (x : α ⊕ β) => x.isRight = true) t

@[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

@[simp]

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

@[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

@[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

@[simp]

theorem RoseTree.traceDepthSum_node {α : 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

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

theorem RoseTree.traceDepthSum_perm {α : Type u_1} {β : Type u_2} {t s : RoseTree (α ⊕ β)} (h : t.Perm 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

theorem RoseTree.traceLeafCount_le_numNodes {α : Type u_1} {β : Type u_2} (t : RoseTree (α ⊕ β)) : t.traceLeafCount ≤ t.numNodes

theorem RoseTree.traceLeafCount_lt_numNodes_of_inl {α : Type u_1} {β : Type u_2} (a : α) (cs : List (RoseTree (α ⊕ β))) : (node (Sum.inl a) cs).traceLeafCount < (node (Sum.inl a) cs).numNodes

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

MCB's letter vocabulary for the generic measures

def RootedTree.Nonplanar.accCount {α : Type u_1} : Nonplanar α → ℕ

MCB's accessible-term count: the edge count (every non-root vertex is an accessible term).

Equations

• RootedTree.Nonplanar.accCount = RootedTree.Nonplanar.numEdges

@[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_add_one {α : Type u_1} (t : Nonplanar α) : t.accCount + 1 = t.numNodes

theorem RootedTree.Nonplanar.accCount_node {α : Type u_1} (a : α) (F : Multiset (Nonplanar α)) : (node a F).accCount = (Multiset.map numNodes F).sum

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

def RootedTree.Nonplanar.accCountP {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : Nonplanar α) : ℕ

Accessible terms discounting the p-leaves. Truncated subtraction covers the single-p-leaf tree, whose root is its one leaf.

Equations

• RootedTree.Nonplanar.accCountP p t = t.numEdges - RootedTree.Nonplanar.leafCountP p t

theorem RootedTree.Nonplanar.accCountP_node_pair {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (l r : Nonplanar α) (hpa : ¬p a) (hl : leafCountP p l < l.numNodes) (hr : leafCountP p r < r.numNodes) : accCountP p (node a {l, r}) = accCountP p l + accCountP p r + 2

Adjoining a root (not counted by p) above a pair adds two discounted accessible terms.

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

The number of Sum.inr-labeled (trace-marker) leaves of a nonplanar tree.

Equations

• RootedTree.Nonplanar.traceLeafCount = RootedTree.Nonplanar.leafCountP fun (x : α ⊕ β) => x.isRight = true

@[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

@[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

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

The depth-weighted trace-marker count of a nonplanar tree.

Equations

• RootedTree.Nonplanar.traceDepthSum = RootedTree.Nonplanar.leafDepthSumP fun (x : α ⊕ β) => x.isRight = true

@[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

theorem RootedTree.Nonplanar.traceLeafCount_lt_numNodes_of_rootInl {α : Type u_1} {β : Type u_2} (t : Nonplanar (α ⊕ β)) (x : α) (h : t.rootValue = Sum.inl x) : t.traceLeafCount < t.numNodes

theorem RootedTree.Nonplanar.traceLeafCount_le_traceDepthSum_of_rootInl {α : Type u_1} {β : Type u_2} (t : Nonplanar (α ⊕ β)) (x : α) (h : t.rootValue = Sum.inl x) : t.traceLeafCount ≤ t.traceDepthSum

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

The trace-excluding accessible-term count αᶜ(T) = α(T) − #traceLeaves(T).

Equations

• RootedTree.Nonplanar.accCountC = RootedTree.Nonplanar.accCountP fun (x : α ⊕ β) => x.isRight = true

@[simp]

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

@[simp]

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

theorem RootedTree.Nonplanar.accCountC_eq {α : Type u_1} {β : Type u_2} (t : Nonplanar (α ⊕ β)) : t.accCountC = t.accCount - t.traceLeafCount

theorem RootedTree.Nonplanar.traceLeafCount_le_accCount {α : Type u_1} {β : Type u_2} (t : Nonplanar (α ⊕ β)) (h : t.traceLeafCount < t.numNodes) : t.traceLeafCount ≤ t.accCount

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 (MCB Lemma 1.6.3, eq. 1.6.5).

MCB's letter vocabulary for the forest measures

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

The number of component trees of a workspace (MCB's zeroth Betti number).

Equations

• RootedTree.Forest.b₀ = Multiset.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} : Multiset (Nonplanar α) → ℕ

MCB's workspace measure α: the total accessible-term (edge) count.

Equations

• RootedTree.Forest.alpha = RootedTree.Forest.numEdges

@[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 α)) : ℕ

MCB's workspace size σ = b₀ + α: the total vertex count (sigma_eq_sum_numNodes).

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_singleton {α : Type u_1} (T : Nonplanar α) : sigma {T} = T.numNodes

@[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

sigma is the total vertex count: the forest case of #V = b₀ + #E.

def RootedTree.Forest.alphaP {α : Type u_1} (p : α → Prop) [DecidablePred p] (F : Multiset (Nonplanar α)) : ℕ

Discounted accessible terms across a workspace.

Equations

• RootedTree.Forest.alphaP p F = (Multiset.map (RootedTree.Nonplanar.accCountP p) F).sum

@[simp]

theorem RootedTree.Forest.alphaP_zero {α : Type u_1} (p : α → Prop) [DecidablePred p] : alphaP p 0 = 0

@[simp]

theorem RootedTree.Forest.alphaP_cons {α : Type u_1} (p : α → Prop) [DecidablePred p] (T : Nonplanar α) (F : Multiset (Nonplanar α)) : alphaP p (T ::ₘ F) = Nonplanar.accCountP p T + alphaP p F

@[simp]

theorem RootedTree.Forest.alphaP_singleton {α : Type u_1} (p : α → Prop) [DecidablePred p] (T : Nonplanar α) : alphaP p {T} = Nonplanar.accCountP p T

@[simp]

theorem RootedTree.Forest.alphaP_add {α : Type u_1} (p : α → Prop) [DecidablePred p] (F G : Multiset (Nonplanar α)) : alphaP p (F + G) = alphaP p F + alphaP p G

def RootedTree.Forest.sigmaP {α : Type u_1} (p : α → Prop) [DecidablePred p] (F : Multiset (Nonplanar α)) : ℕ

Discounted workspace size: components plus discounted accessible terms. Unlike sigma, this is not the vertex count when counted leaves exist.

Equations

• RootedTree.Forest.sigmaP p F = RootedTree.Forest.b₀ F + RootedTree.Forest.alphaP p F

@[simp]

theorem RootedTree.Forest.sigmaP_zero {α : Type u_1} (p : α → Prop) [DecidablePred p] : sigmaP p 0 = 0

@[simp]

theorem RootedTree.Forest.sigmaP_cons {α : Type u_1} (p : α → Prop) [DecidablePred p] (T : Nonplanar α) (F : Multiset (Nonplanar α)) : sigmaP p (T ::ₘ F) = Nonplanar.accCountP p T + 1 + sigmaP p F

@[simp]

theorem RootedTree.Forest.sigmaP_singleton {α : Type u_1} (p : α → Prop) [DecidablePred p] (T : Nonplanar α) : sigmaP p {T} = Nonplanar.accCountP p T + 1

@[simp]

theorem RootedTree.Forest.sigmaP_add {α : Type u_1} (p : α → Prop) [DecidablePred p] (F G : Multiset (Nonplanar α)) : sigmaP p (F + G) = sigmaP p F + sigmaP p G

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 = RootedTree.Forest.alphaP (fun (x : α ⊕ β) => x.isRight = true) F

theorem RootedTree.Forest.alphaC_eq {α : Type u_1} {β : Type u_2} (F : Multiset (Nonplanar (α ⊕ β))) : alphaC F = (Multiset.map 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); not the vertex count for contraction quotients (σᶜ ≠ #V, MCB p. 66).

Equations

• RootedTree.Forest.sigmaC F = RootedTree.Forest.sigmaP (fun (x : α ⊕ β) => x.isRight = true) F

theorem RootedTree.Forest.sigmaC_eq {α : Type u_1} {β : Type u_2} (F : Multiset (Nonplanar (α ⊕ β))) : sigmaC F = b₀ F + 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_singleton {α : Type u_1} {β : Type u_2} (T : Nonplanar (α ⊕ β)) : sigmaC {T} = T.accCountC + 1

@[simp]

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