Admissibility implies the Proposition 5.9 diameter hypothesis

Paper §5.4 invokes the cluster-diameter estimate from Proposition 5.6 before applying Proposition 5.9. The geometric estimate uses the child-count scale tildeScale; the latter is bounded termwise by accumulatedScale because gammaInf counts every child and possibly additional leaf multiplicities.

theorem Anderson4D.tildeScale_le_accumulatedScale {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (v : t.VPos) : tildeScale Nm v ≤ ↑(accumulatedScale Nm mu v)

The multiplicity-weighted accumulated scale dominates the purely tree-geometric cluster scale.

theorem Anderson4D.IsAdmissible.satisfiesSubtreeDiameter {t : PlaneTree} {Nm : t.HeppMarking} {M : ℕ} {z : HeppLeaf t → Fin 4 → ℤ} (hadm : IsAdmissible Nm M z) (mu : t.Multiplicities) : SatisfiesSubtreeDiameter Nm mu z

An admissible leaf embedding satisfies condition (5.32) for every choice of leaf multiplicities.