The order of a homogeneous harmonic map has denominator dividing the Weyl group

Disproved

HarmonicBuildingKL.homogeneousOrderDenominatorDividesWeylWD

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

coxetereuclidean-buildingsharmonic-maps

If $h$ is a nonconstant homogeneous harmonic map of order $\alpha$ from the plane into a conical Euclidean building of type $W$ carrying its $\Delta_{\mathrm{mod}}$ -direction structure, then

\alpha=\frac{m}{k}\qquad\text{for positive integers }m,k\text{ with }k\mid|W| .

Role. This is the homogeneous case of the classification of orders, and by the blow-up reduction it is equivalent to the general case: the order of an arbitrary nonconstant harmonic map into a building equals the order of its tangent map, which is homogeneous on a conical building of the same type. It is the statement in which the arithmetic constraint on the order first appears.

The argument. The dichotomy for homogeneous maps splits into two branches. In the first, $\alpha=m/2$ for an integer $m\ge2$ ; since the Weyl group of a Euclidean Coxeter complex contains a reflection, $2$ divides $|W|$ , so the answer has the required form with $k=2$ . In the second, the image of the unit circle lies at constant distance $L$ from the cone point; then the length of that image is $2\pi\alpha L$ , and feeding this into the billiards analysis of the constant-distance branch produces the denominator dividing $|W|$ directly.

Retired 2026-09-07 — disproved, false as formalized. Do not use as a dependency.

The defect is in the shared definition layer, not in the mathematics of Breiner--Dees. IsPlanarKSHarmonicOn (Def_frame_2026_harmonic_building_conical) is defined purely through Lebesgue integrals -- ksEnergy, ksApproxEnergy, IsKSSobolevOn, SameKSTraceOnCircle -- and, unlike the goal-level predicate IsKSHarmonic, it does not require ContinuousOn. An a.e.-constant map therefore qualifies as "harmonic", and altering a map on a Lebesgue-null, dilation-invariant set (a ray) preserves every hypothesis -- IsHomogeneousOfOrderOn and NonconstantOn included, both being pointwise -- while destroying the pointwise conclusion. The same gap admits order alpha = 0 for nonconstant maps, which the source excludes.

A faithful restatement needs Continuous h (or the conclusion attached to the continuous representative) together with 0 < alpha. No corrected replacement node exists yet.

Preamble

import Definitions.Def_euclidean_building_directions
import Definitions.Def_frame_2026_harmonic_building_conical

Formal statement

namespace HarmonicBuildingKL

open HarmonicBuilding EuclideanBuildingDirections

universe v

theorem homogeneousOrderDenominatorDividesWeylWD
    {N : ℕ} (C : EuclideanCoxeterData N) (M : ConicalBuildingModel.{v} N C)
    (BM : BuildingWithDirections N C M.carrier)
    (h : ℂ → M.carrier) (alpha : ℝ)
    (hhom : IsHomogeneousOfOrderOn M Set.univ h 0 alpha)
    (hharm : IsPlanarKSHarmonicOn Set.univ h)
    (hnc : NonconstantOn h Set.univ) :
    ∃ m k : ℕ, 0 < m ∧ 0 < k ∧
      k ∣ Fintype.card C.weyl ∧ alpha = (m : ℝ) / (k : ℝ) := by sorry

end HarmonicBuildingKL

Source

Theorem 2.15 of C. Breiner and S. Dees, Harmonic maps into Euclidean buildings, arXiv:2604.16608: for a nonconstant homogeneous harmonic map of order alpha from the plane into a conical Euclidean building of type W, alpha = m/k with k dividing the order of W.

View graph