Cluster diameter from the Hepp-tree link condition

This file formalizes paper §5.3 Step 4(a), equation (5.22a). For a vertex v, tildeScale Nm v is the sum of

childCount(t,u) * scaleN(Nm,u)

over branching descendants u of v (including v when it branches). The paper writes the same index condition as “v is an ancestor of u”. Here ancestry is the prefix relation on vertex-position lists.

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

Branching descendants of v, including v itself when it branches.

Equations

• Anderson4D.branchDescendants v = {u ∈ t.BranchNodes | ↑v <+: ↑u}

@[simp]

theorem Anderson4D.mem_branchDescendants {t : PlaneTree} {v u : t.VPos} : u ∈ branchDescendants v ↔ u ∈ t.BranchNodes ∧ ↑v <+: ↑u

noncomputable def Anderson4D.tildeScale {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : ℝ

The accumulated scale from (5.22a). It is ℝ-valued because it is compared directly with znorm; every summand is the coercion of the paper's integer quantity #children(u) N_u.

Equations

• Anderson4D.tildeScale Nm v = ∑ u ∈ Anderson4D.branchDescendants v, ↑(t.childCount ↑u) * ↑(Anderson4D.scaleN Nm u)

theorem Anderson4D.tildeScale_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : 0 ≤ tildeScale Nm v

theorem Anderson4D.tildeScale_mono_of_ancestor {t : PlaneTree} (Nm : t.HeppMarking) {v w : t.VPos} (hvw : ↑v <+: ↑w) : tildeScale Nm w ≤ tildeScale Nm v

Moving downward in the tree can only remove summands from tildeScale.

theorem Anderson4D.card_childrenOf (t : PlaneTree) (v : t.VPos) : (childrenOf v).card = t.childCount ↑v

The finite set childrenOf v has the expected cardinality.

theorem Anderson4D.clusterDiameter_branch_step {t : PlaneTree} {Nm : t.HeppMarking} {M : ℕ} {z : ↥t.Leaves → Fin 4 → ℤ} {v : t.VPos} (hv : v ∈ t.BranchNodes) (hadm : IsAdmissible Nm M z) (hlocal : ∀ c ∈ childrenOf v, ∀ l ∈ leavesUnder c, ∀ l' ∈ leavesUnder c, znorm (z l - z l') ≤ tildeScale Nm c) {l l' : ↥t.Leaves} (hl : l ∈ leavesUnder v) (hl' : l' ∈ leavesUnder v) : znorm (z l - z l') ≤ tildeScale Nm v

Recursive branch step behind (5.22a): if the diameter estimate is known inside every immediate child cluster, the LinkedChildren condition gives the estimate at the branch itself. A simple path in the finite child-link graph is used, so every child-cluster contribution is charged at most once and the number of link edges is strictly smaller than childCount t v.1.

theorem Anderson4D.clusterDiameter_le_tildeScale {t : PlaneTree} {Nm : t.HeppMarking} {M : ℕ} {z : ↥t.Leaves → Fin 4 → ℤ} (hadm : IsAdmissible Nm M z) (v : t.VPos) {l l' : ↥t.Leaves} (hl : l ∈ leavesUnder v) (hl' : l' ∈ leavesUnder v) : znorm (z l - z l') ≤ tildeScale Nm v

Cluster diameter bound, paper (5.22a). In an admissible embedding, any two leaves below v are separated by at most the accumulated descendant scale tildeScale Nm v. The statement also covers non-Hepp-valid carriers: a unary vertex simply inherits the estimate from its unique child.