Linear covers of admissible Hepp clusters

Paper §5.3 Step 4(b) covers the leaf cluster below v by at most

3 * (1 + tildeScale Nm v / R)

balls of radius R. The proof is split into two reusable finite statements: a polygonal-tour cover lemma, and the extraction of a tour of total length at most 2 * tildeScale from the recursive LinkedChildren structure.

A double traversal of a finite connected graph

Mathlib does not currently expose the usual doubled-edge tour of a spanning tree. The following finite induction supplies exactly that statement. It removes one vertex while preserving connectedness, recursively tours the induced complement, rotates the tour to a neighbour of the removed vertex, and appends the two-edge excursion to that vertex.

theorem Anderson4D.exists_double_tour {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (hG : G.Connected) : ∃ (r : V) (p : G.Walk r r), p.support.toFinset = Finset.univ ∧ ∀ (e : Sym2 V), List.count e p.edges ≤ 2

A finite connected graph has a closed walk visiting all its vertices in which every undirected edge is used at most twice.

def Anderson4D.chainLengthFrom {α : Type u_1} (d : α → α → ℝ) (a : α) : List α → ℝ

Length of a finite polygonal chain after an initial point a.

Equations

• Anderson4D.chainLengthFrom d a [] = 0
• Anderson4D.chainLengthFrom d a (b :: bs) = d a b + Anderson4D.chainLengthFrom d b bs

def Anderson4D.chainLength {α : Type u_1} (d : α → α → ℝ) : List α → ℝ

Total consecutive-edge length of a finite list.

Equations

• Anderson4D.chainLength d [] = 0
• Anderson4D.chainLength d (b :: bs) = Anderson4D.chainLengthFrom d b bs

def Anderson4D.sym2Weight {α : Type u_1} (d : α → α → ℝ) (hsymm : ∀ (a b : α), d a b = d b a) : Sym2 α → ℝ

The weight induced on an undirected edge by a symmetric cost.

Equations

• Anderson4D.sym2Weight d hsymm = Sym2.lift ⟨d, hsymm⟩

@[simp]

theorem Anderson4D.sym2Weight_mk {α : Type u_1} (d : α → α → ℝ) (hsymm : ∀ (a b : α), d a b = d b a) (a b : α) : sym2Weight d hsymm s(a, b) = d a b

@[simp]

theorem Anderson4D.chainLength_nil {α : Type u_1} (d : α → α → ℝ) : chainLength d [] = 0

@[simp]

theorem Anderson4D.chainLength_singleton {α : Type u_1} (d : α → α → ℝ) (a : α) : chainLength d [a] = 0

@[simp]

theorem Anderson4D.chainLength_cons_cons {α : Type u_1} (d : α → α → ℝ) (a b : α) (xs : List α) : chainLength d (a :: b :: xs) = d a b + chainLength d (b :: xs)

theorem Anderson4D.chainLength_map {α : Type u_1} {β : Type u_2} (d : β → β → ℝ) (f : α → β) (xs : List α) : chainLength d (List.map f xs) = chainLength (fun (x y : α) => d (f x) (f y)) xs

Consecutive length commutes with mapping the vertices of a chain.

theorem Anderson4D.chainLength_walk_support {V : Type u_2} {G : SimpleGraph V} (d : V → V → ℝ) (hsymm : ∀ (a b : V), d a b = d b a) {a b : V} (p : G.Walk a b) : chainLength d p.support = (List.map (sym2Weight d hsymm) p.edges).sum

The length of a graph walk's support list is the sum of the weights of its edge list.

theorem Anderson4D.exists_short_tour_of_connected_graph {V : Type u} [Fintype V] [DecidableEq V] (d : V → V → ℝ) (hd : ∀ (a b : V), 0 ≤ d a b) (hsymm : ∀ (a b : V), d a b = d b a) (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) : ∃ (xs : List V), xs ≠ [] ∧ xs.toFinset = Finset.univ ∧ chainLength d xs ≤ 2 * ∑ e ∈ G.edgeFinset, sym2Weight d hsymm e

A connected weighted finite graph has a vertex tour whose polygonal length is at most twice its total edge weight.

theorem Anderson4D.chainLength_nonneg {α : Type u_1} (d : α → α → ℝ) (hd : ∀ (a b : α), 0 ≤ d a b) (xs : List α) : 0 ≤ chainLength d xs

theorem Anderson4D.chainLength_mono_sublist {α : Type u_1} (d : α → α → ℝ) (hd : ∀ (a b : α), 0 ≤ d a b) (htri : ∀ (a b c : α), d a c ≤ d a b + d b c) {xs ys : List α} (hsub : xs.Sublist ys) : chainLength d xs ≤ chainLength d ys

Shortcutting a polygonal chain cannot increase its length.

theorem Anderson4D.exists_cover_of_chain {α : Type u_1} [DecidableEq α] (d : α → α → ℝ) (hd : ∀ (a b : α), 0 ≤ d a b) (hself : ∀ (a : α), d a a = 0) (hsymm : ∀ (a b : α), d a b = d b a) (htri : ∀ (a b c : α), d a c ≤ d a b + d b c) (xs : List α) (hxs : xs ≠ []) {R : ℝ} (hR : 0 < R) : ∃ Q ⊆ xs.toFinset, (∀ x ∈ xs.toFinset, ∃ q ∈ Q, d x q ≤ R) ∧ ↑Q.card ≤ 1 + chainLength d xs / R

A finite polygonal tour admits a linear-cardinality radius-R cover. This is the metric-combinatorial core of Step 4(b).

def Anderson4D.leafDistance {t : PlaneTree} (z : ↥t.Leaves → Fin 4 → ℤ) (l l' : ↥t.Leaves) : ℝ

Distance between two embedded leaves.

Equations

• Anderson4D.leafDistance z l l' = Anderson4D.znorm (z l - z l')

def Anderson4D.clusterLeafDistance {t : PlaneTree} (z : ↥t.Leaves → Fin 4 → ℤ) (v : t.VPos) (a b : ↥(leavesUnder v)) : ℝ

The metric on the leaves below a fixed vertex, keeping the proof-relevant subtype needed to speak about a graph on exactly that cluster.

Equations

• Anderson4D.clusterLeafDistance z v a b = Anderson4D.leafDistance z ↑a ↑b

noncomputable def Anderson4D.clusterNetworkLength {t : PlaneTree} (z : ↥t.Leaves → Fin 4 → ℤ) (v : t.VPos) (G : SimpleGraph ↥(leavesUnder v)) : ℝ

Total geometric length of a finite graph connecting the leaves below v. Its edges are measured by the actual znorm distance of their embedded endpoints.

Equations

• Anderson4D.clusterNetworkLength z v G = ∑ e ∈ G.edgeFinset, Anderson4D.sym2Weight (Anderson4D.clusterLeafDistance z v) ⋯ e

def Anderson4D.HasClusterNetwork {t : PlaneTree} (Nm : t.HeppMarking) (z : ↥t.Leaves → Fin 4 → ℤ) (v : t.VPos) : Prop

The exact geometric certificate underlying §5.3 Step 4(b): the leaf cluster has a connected network of total length at most its accumulated Hepp scale. The recursive LinkedChildren construction is intended to produce this certificate by joining the child certificates with one link per edge of a child spanning tree.

Equations

• Anderson4D.HasClusterNetwork Nm z v = ∃ (G : SimpleGraph ↥(Anderson4D.leavesUnder v)), G.Connected ∧ Anderson4D.clusterNetworkLength z v G ≤ Anderson4D.tildeScale Nm v

def Anderson4D.IsClusterTour {t : PlaneTree} (Nm : t.HeppMarking) (z : ↥t.Leaves → Fin 4 → ℤ) (v : t.VPos) (xs : List ↥t.Leaves) : Prop

Exact tour certificate needed for the cluster-cover claim: the list visits precisely the leaves below v (repetitions allowed), and its total polygonal length is at most twice the accumulated Hepp scale. The factor two is the standard traversal of each edge of a connecting tree in both directions.

Equations

• Anderson4D.IsClusterTour Nm z v xs = (xs ≠ [] ∧ xs.toFinset = Anderson4D.leavesUnder v ∧ Anderson4D.chainLength (Anderson4D.leafDistance z) xs ≤ 2 * Anderson4D.tildeScale Nm v)

theorem Anderson4D.exists_clusterCover_of_tour {t : PlaneTree} {Nm : t.HeppMarking} {M : ℕ} {z : ↥t.Leaves → Fin 4 → ℤ} (hadm : IsAdmissible Nm M z) (v : t.VPos) (xs : List ↥t.Leaves) (htour : IsClusterTour Nm z v xs) {R : ℝ} (hR : 0 < R) : ∃ Q ⊆ Finset.image z (leavesUnder v), (∀ l ∈ leavesUnder v, ∃ q ∈ Q, znorm (z l - q) ≤ R) ∧ ↑Q.card ≤ 3 * (1 + tildeScale Nm v / R)

Step 4(b) once the precise finite tour certificate has been extracted from LinkedChildren. This lemma already produces lattice-valued centers, not merely leaf indices, and has exactly the constant in the paper.

theorem Anderson4D.exists_clusterCover_of_network {t : PlaneTree} {Nm : t.HeppMarking} {M : ℕ} {z : ↥t.Leaves → Fin 4 → ℤ} (hadm : IsAdmissible Nm M z) (v : t.VPos) (hnetwork : HasClusterNetwork Nm z v) {R : ℝ} (hR : 0 < R) : ∃ Q ⊆ Finset.image z (leavesUnder v), (∀ l ∈ leavesUnder v, ∃ q ∈ Q, znorm (z l - q) ≤ R) ∧ ↑Q.card ≤ 3 * (1 + tildeScale Nm v / R)

Cluster cover from a connected network, §5.3 Step 4(b). A connected leaf network of total length at most tildeScale yields the paper's lattice-centre cover with the exact stated constant. This is the precise metric-tree main lemma consumed by the recursive LinkedChildren construction; no ambient box-counting loss is used.