Simple and compound leaves: paper Def 5.8 and (5.30)–(5.31).

def Anderson4D.compoundLeaves (t : PlaneTree) (C : Finset t.VPos) : Finset t.VPos

Compound leaves; vertices outside Leaves t are ignored.

Equations

• Anderson4D.compoundLeaves t C = t.Leaves ∩ C

def Anderson4D.simpleLeaves (t : PlaneTree) (C : Finset t.VPos) : Finset t.VPos

Simple leaves are precisely the non-compound leaves.

Equations

• Anderson4D.simpleLeaves t C = t.Leaves \ C

def Anderson4D.leafChildren {t : PlaneTree} (v : t.VPos) : Finset t.VPos

Equations

• Anderson4D.leafChildren v = Anderson4D.childrenOf v ∩ t.Leaves

def Anderson4D.branchChildren {t : PlaneTree} (v : t.VPos) : Finset t.VPos

Equations

• Anderson4D.branchChildren v = Anderson4D.childrenOf v ∩ t.BranchNodes

def Anderson4D.gamma2 {t : PlaneTree} (mu : t.Multiplicities) (C : Finset t.VPos) (v : t.VPos) : ℕ

Paper (5.30): simple leaves count twice, compound leaves fully.

Equations

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

def Anderson4D.gammaInf {t : PlaneTree} (mu : t.Multiplicities) (v : t.VPos) : ℕ

Paper (5.30): every leaf child counts with full multiplicity.

Equations

• Anderson4D.gammaInf mu v = (Anderson4D.childrenOf v).card + ∑ l ∈ Anderson4D.leafChildren v, (mu.m l - 1)

theorem Anderson4D.simple_union_compound (t : PlaneTree) (C : Finset t.VPos) : simpleLeaves t C ∪ compoundLeaves t C = t.Leaves

theorem Anderson4D.disjoint_simple_compound (t : PlaneTree) (C : Finset t.VPos) : Disjoint (simpleLeaves t C) (compoundLeaves t C)

theorem Anderson4D.gamma2_le_gammaInf {t : PlaneTree} (mu : t.Multiplicities) (C : Finset t.VPos) (v : t.VPos) : gamma2 mu C v ≤ gammaInf mu v

The inequality following (5.30), using m_l ≥ 2.

theorem Anderson4D.card_leafChildren_add_branchChildren {t : PlaneTree} (ht : t.isValid = true) (v : t.VPos) : (leafChildren v).card + (branchChildren v).card = (childrenOf v).card

theorem Anderson4D.gamma2_allSimple {t : PlaneTree} (mu : t.Multiplicities) (v : t.VPos) : gamma2 mu ∅ v = (childrenOf v).card + (leafChildren v).card

def Anderson4D.allSimpleLhsExponent {t : PlaneTree} (v : t.VPos) : ℤ

Collected exponent of N_v on the left of paper (5.31).

Equations

• Anderson4D.allSimpleLhsExponent v = -4 * ↑(Anderson4D.childrenOf v).card + 4 - if v = t.rootV then 2 else 0

def Anderson4D.allSimpleRhsExponent {t : PlaneTree} (mu : t.Multiplicities) (v : t.VPos) : ℤ

Collected exponent on the right of (5.31), including the parent ratios.

Equations

• Anderson4D.allSimpleRhsExponent mu v = (-2 * ↑(Anderson4D.gamma2 mu ∅ v) + 2 + if v = t.rootV then 0 else 2) - 2 * ↑(Anderson4D.branchChildren v).card

theorem Anderson4D.allSimple_exponent_identity {t : PlaneTree} (ht : t.isValid = true) (mu : t.Multiplicities) (v : t.VPos) : allSimpleLhsExponent v = allSimpleRhsExponent mu v

The nodewise power count printed immediately after (5.31).

theorem Anderson4D.allSimple_product_identity {t : PlaneTree} (ht : t.isValid = true) (mu : t.Multiplicities) (N : t.VPos → ℝ) (_hN : ∀ v ∈ t.BranchNodes, 0 < N v) : ∏ v ∈ t.BranchNodes, N v ^ allSimpleLhsExponent v = ∏ v ∈ t.BranchNodes, N v ^ allSimpleRhsExponent mu v

Positive-real zpow form of (5.31), with parent-ratio powers collected.

theorem Anderson4D.mem_childrenOf_iff_ne_root_and_parentV_eq {t : PlaneTree} {v w : t.VPos} : w ∈ childrenOf v ↔ w ≠ t.rootV ∧ PlaneTree.parentV w = v

A vertex is a child of v exactly when it is non-root and has parent v. This bridges the path-based childrenOf definition with incidence counting in (5.31).

theorem Anderson4D.branchChildren_eq_parentFiber {t : PlaneTree} (p : t.VPos) : branchChildren p = {w ∈ t.BranchNodes.erase t.rootV | PlaneTree.parentV w = p}

The branch children of p are the fiber over p of the parent map on non-root branch nodes.

theorem Anderson4D.parent_incidence_product {t : PlaneTree} (ht : t.isValid = true) (N : t.VPos → ℝ) : ∏ v ∈ t.BranchNodes.erase t.rootV, N (PlaneTree.parentV v) ^ 2 = ∏ p ∈ t.BranchNodes, N p ^ (2 * ↑(branchChildren p).card)

Parent-incidence regrouping: every denominator scale in the ratio product is counted once for each branch child.

theorem Anderson4D.nonroot_branch_product {t : PlaneTree} (hroot : t.rootV ∈ t.BranchNodes) (N : t.VPos → ℝ) : ∏ v ∈ t.BranchNodes.erase t.rootV, N v ^ 2 = ∏ p ∈ t.BranchNodes, N p ^ if p = t.rootV then 0 else 2

The numerator of the parent-ratio product contributes power two at every non-root branch node and power zero at the root.

theorem Anderson4D.parent_ratio_product {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (N : t.VPos → ℝ) (hN : ∀ v ∈ t.BranchNodes, 0 < N v) : ∏ v ∈ t.BranchNodes.erase t.rootV, (N v / N (PlaneTree.parentV v)) ^ 2 = ∏ p ∈ t.BranchNodes, N p ^ ((if p = t.rootV then 0 else 2) - 2 * ↑(branchChildren p).card)

The raw parent-ratio product regrouped as one power at each branch node. This is the incidence step implicit in the paper's power count after (5.31).

theorem Anderson4D.allSimple_lhs_product_eq_collected {t : PlaneTree} (hroot : t.rootV ∈ t.BranchNodes) (N : t.VPos → ℝ) (hN : ∀ v ∈ t.BranchNodes, 0 < N v) : (∏ v ∈ t.BranchNodes, N v ^ (-4 * (↑(childrenOf v).card - 1))) * N t.rootV ^ (-2) = ∏ v ∈ t.BranchNodes, N v ^ allSimpleLhsExponent v

The uncollected left side of (5.31), including its extra root factor, equals the product with the collected left exponent.

theorem Anderson4D.allSimple_rhs_product_eq_collected {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (N : t.VPos → ℝ) (hN : ∀ v ∈ t.BranchNodes, 0 < N v) : (∏ v ∈ t.BranchNodes, N v ^ (-2 * (↑(gamma2 mu ∅ v) - 1))) * ∏ v ∈ t.BranchNodes.erase t.rootV, (N v / N (PlaneTree.parentV v)) ^ 2 = ∏ v ∈ t.BranchNodes, N v ^ allSimpleRhsExponent mu v

The uncollected right side of (5.31), including its parent ratios, equals the product with the collected right exponent.

theorem Anderson4D.allSimple_direct_product_identity {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (N : t.VPos → ℝ) (hN : ∀ v ∈ t.BranchNodes, 0 < N v) : (∏ v ∈ t.BranchNodes, N v ^ (-4 * (↑(childrenOf v).card - 1))) * N t.rootV ^ (-2) = (∏ v ∈ t.BranchNodes, N v ^ (-2 * (↑(gamma2 mu ∅ v) - 1))) * ∏ v ∈ t.BranchNodes.erase t.rootV, (N v / N (PlaneTree.parentV v)) ^ 2

Paper (5.31) in its direct, uncollected form. The hypotheses state that the Hepp tree is valid, its root is a branch node, and all branch scales are positive.