Uniform scale bounds for realizing Hepp trees

Paper Lemma 5.5 requires the marks of a realizing tree to satisfy 1 < N_v ≲ M. The lower bound is part of HeppMarking; this file proves the uniform upper bound N_v ≤ 4 M directly from admissibility in the box [-M, M]⁴, and packages it with the general realizing-tree construction.

theorem Anderson4D.scaleN_le_four_mul_of_isAdmissible {t : PlaneTree} {Nm : t.HeppMarking} {M : ℕ} {z : ↥t.Leaves → Fin 4 → ℤ} (hadm : IsAdmissible Nm M z) {v : t.VPos} (hv : v ∈ t.BranchNodes) : ↑(scaleN Nm v) ≤ 4 * ↑M

Every branch scale of an admissible embedding in [-M,M]⁴ is at most 4M. This is the explicit N_v ≲ M part of paper Lemma 5.5.

Choose two children of v. Connectedness supplies a nontrivial link between two (possibly intermediate) distinct children, hence leaves below those two children. Their LCA is v; admissible separation gives N_v / 2 as a lower bound for their distance, while the box gives the upper bound 2M.

theorem Anderson4D.rdec_exists_realizing_marked_tree_with_scale (M : ℕ) (Z : Finset (Fin 4 → ℤ)) (hZ : Z.Nonempty) (hbound : ∀ x ∈ Z, ∀ (i : Fin 4), |x i| ≤ ↑M) : ∃ (t : PlaneTree), t.isValid = true ∧ ∃ (Nm : t.HeppMarking), Realizes Nm M Z ∧ t.leafCount = Z.card ∧ ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M

Paper-facing wrapper around the greedy realizing-tree construction: besides validity, realization, and the exact leaf count, every branch mark is bounded by 4M.