Lemma 2.14 — the order is realized by a homogeneous map into a conical building

Proved

HarmonicBuilding.orderReducesToHomogeneous

by Shuze Chen · Aug 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

calculus-of-variationscoxeter-groupseuclidean-buildingsgeometric-analysisharmonic-maps

Throughout, $W$ is the finite Weyl group of a Euclidean Coxeter datum on an $N$ -dimensional model apartment, and a conical Euclidean building of type $W$ is a complete Euclidean building carrying a metric cone structure with cone point $0_X$ . A map $h$ of the plane into such a building is homogeneous of order $\alpha$ about $x_0$ when $h(x_0)=0_X$ and

h(x_0+\lambda z)=\lambda^{\alpha}\,h(x_0+z)\qquad\text{for all }\lambda>0,

the right side denoting dilation about the cone point.

This is the tangent-map reduction. Let $S$ be a domain in a Riemann surface, $X$ a Euclidean building of type $W$ , and $u:S\to X$ a nonconstant Korevaar–Schoen harmonic map whose order at a point $x_0$ equals $\alpha$ . The assertion is that there exist a conical Euclidean building $X'$ of the same type $W$ and a nonconstant homogeneous harmonic map

u_*:\mathbb{R}^2 \longrightarrow X'

of the same order $\alpha$ about the origin.

The mechanism is blow-up: rescaling $u$ around $x_0$ at a sequence of shrinking radii, with the target rescaled correspondingly, produces in the limit a map into the tangent cone at $u(x_0)$ . Two facts make the statement useful. Rescaling does not change the order, so $u_*$ inherits $\alpha$ exactly; and the tangent cone of a Euclidean building of type $W$ is again a Euclidean building of type $W$ , so the Coxeter data — and in particular the number $|W|$ that the final arithmetic conclusion refers to — is unchanged.

The effect of this reduction is to replace an arbitrary harmonic map on a Riemann surface by a scale-invariant model on the plane. Everything after it is a statement about homogeneous maps.

Formalization Note. The source states the conclusion for a map on the unit ball $B_1(0)\subset\mathbb{R}^2$ . The statement here asks for the homogeneous model on the whole plane, which is the setting of Definition 2.13 itself and is equivalent: a map homogeneous of order $\alpha$ on a ball about the origin extends canonically to the plane by its own scaling relation, and energy minimization is scale invariant.

Preamble

import Definitions.Def_frame_2026_harmonic_building_conical

Formal statement

namespace HarmonicBuilding

open scoped Manifold

universe v w

theorem orderReducesToHomogeneous
    {N : ℕ} (C : EuclideanCoxeterData N)
    {X : Type v} {S : Type w}
    [MetricSpace X] [CompleteSpace X] [MeasurableSpace X] [BorelSpace X]
    [TopologicalSpace S] [T2Space S] [SecondCountableTopology S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    (B : EuclideanBuildingData N C X)
    (D : RiemannSurfaceDomain S) (u : S → X) (x₀ : D.Point)
    (hu : IsKSHarmonic D u) (hnc : NonconstantOn u D.carrier)
    (alpha : ℝ) (halpha : HasOrderAt D u x₀ alpha) :
    ∃ M : ConicalBuildingModel.{v} N C, ∃ h : ℂ → M.carrier,
      IsHomogeneousOfOrderOn M Set.univ h 0 alpha ∧
        IsPlanarKSHarmonicOn Set.univ h ∧
        NonconstantOn h Set.univ := by sorry

end HarmonicBuilding

Source

Christine Breiner and Ben K. Dees, On the Possible Orders of Harmonic Maps into Euclidean Buildings, Calculus of Variations and Partial Differential Equations (2026), arXiv:2604.16608, https://doi.org/10.1007/s00526-026-03375-5, Lemma 2.14 (Section 2), with Definitions 2.9 and 2.11 (tangent maps and intrinsic homogeneity), Remark 2.10 (the order is preserved under rescaling and tangent maps keep the type W), and Definition 2.13.

View graph