Theorem 1.1 — Possible orders of harmonic maps into Euclidean buildings

Open

HarmonicBuilding.possibleOrders

by ShouqiaoWang · Aug 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

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

Let $D$ be a connected domain in a Riemann surface, let $X$ be a complete Euclidean building of Coxeter type $W$ , and let $u:D\to X$ be a nonconstant energy-minimizing harmonic map in the concrete metric-Sobolev sense fixed by the definition bundle. For every $x_0\in D$ , prove that the small-scale energy is finite, the relevant boundary moment is positive, and the frequency quotient has a well-defined order. Moreover, prove that there exist positive integers $m,k$ such that

\operatorname{Ord}_u(x_0)=\frac{m}{k} \qquad\text{and}\qquad k\mid |W|.

If $X$ has rank one, prove the sharper conclusion

\operatorname{Ord}_u(x_0)=\frac{m}{2} \quad\text{for some }m\ge2.

The nonconstant condition is explicit because the standard frequency quotient for a constant map is $0/0$ ; it is also the condition used by the source paper's tangent-map reduction.

Preamble

import Definitions.Def_frame_2026_harmonic_building_interfaces

Formal statement

namespace HarmonicBuilding

open scoped Manifold

theorem possibleOrders
    {N : ℕ} (C : EuclideanCoxeterData N)
    {X S : Type*}
    [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) :
    PossibleOrdersProblem C B D u x₀ := 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), Theorem 1.1 on physical p. 2; definitions and reduction in Section 2: https://doi.org/10.1007/s00526-026-03375-5

View graph