The circle of a homogeneous map turns at angular speed $\alpha$

Disproved

HarmonicBuilding.circleAngularSpeed

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

comparison-geometryeuclidean-buildingsharmonic-mapsmetric-geometry

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
import Definitions.Def_metric_geodesic_angle

Formal statement

namespace HarmonicBuilding

universe v

theorem circleAngularSpeed
    {N : ℕ} (C : EuclideanCoxeterData N) (M : ConicalBuildingModel.{v} N C)
    (h : ℂ → M.carrier) (alpha L : ℝ)
    (hhom : IsHomogeneousOfOrderOn M Set.univ h 0 alpha)
    (hharm : IsPlanarKSHarmonicOn Set.univ h)
    (hnc : NonconstantOn h Set.univ)
    (hconst : ∀ theta : ℝ, dist (h (circlePoint 0 1 theta)) (h 0) = L) :
    ∃ delta : ℝ, 0 < delta ∧ ∀ theta1 theta2 : ℝ, |theta1 - theta2| ≤ delta →
      MetricGeometry.comparisonAngle (h 0)
          (h (circlePoint 0 1 theta1)) (h (circlePoint 0 1 theta2))
        = alpha * |theta1 - theta2| := by sorry

end HarmonicBuilding

Source

C. Breiner and B. K. Dees, On the Possible Orders of Harmonic Maps into Euclidean Buildings, Calc. Var. PDE (2026), arXiv:2604.16608. The apartment representation is the one displayed in the proof of Lemma 3.2 and reused in the proof of Lemma 4.2; the angular reformulation is Lemma 4.2(1).

View graph

The circle of a homogeneous map turns at angular speed α\alphaα

The circle of a homogeneous map turns at angular speed $\alpha$