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

Disproved

HarmonicBuildingKL.homogeneousOrderDenominatorDividesWeylWD

by Shuze Chen · Aug 31, 2026 · Mathlib c5ea003 (Lean v4.30.0)

coxetereuclidean-buildingsharmonic-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_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