A nonconstant homogeneous harmonic map has order $\alpha \ge 1$

Disproved

HarmonicBuilding.homogeneousOrderAtLeastOne

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

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

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_frame_2026_harmonic_building_conical

Formal statement

namespace HarmonicBuilding

universe v

theorem homogeneousOrderAtLeastOne
    {N : ℕ} (C : EuclideanCoxeterData N) (M : ConicalBuildingModel.{v} N C)
    (h : ℂ → M.carrier) (alpha : ℝ)
    (hhom : IsHomogeneousOfOrderOn M Set.univ h 0 alpha)
    (hharm : IsPlanarKSHarmonicOn Set.univ h)
    (hnc : NonconstantOn h Set.univ) :
    1 ≤ alpha := 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, Definition 2.7 and Theorem 2.8 (the order gap), transplanted to the homogeneous setting of Definition 2.13 through the rescaling invariance of Remark 2.10. It supplies the bound m >= 2 in case (1) of Theorem 3.1.

View graph

A nonconstant homogeneous harmonic map has order α≥1\alpha \ge 1α≥1

A nonconstant homogeneous harmonic map has order $\alpha \ge 1$