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

Disproved

HarmonicBuilding.circleAngularSpeed

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

comparison-geometryeuclidean-buildingsharmonic-mapsmetric-geometry

Let $M$ be a conical Euclidean building of type $W$ and $h:\mathbb C\to M$ a nonconstant homogeneous harmonic map of order $\alpha$ about $0$ whose unit circle lies at constant distance $L$ from the cone point $h(0)$ . Then there is a $\delta>0$ such that for $|\theta_1-\theta_2|\le\delta$ ,

\widetilde\angle_{h(0)}\bigl(h(e^{i\theta_1}),\,h(e^{i\theta_2})\bigr)=\alpha\,|\theta_1-\theta_2| .

Role. This is Lemma 4.2(1) of the source: after rescaling the circle into the space of directions at $h(0)$ — whose metric is precisely the angle at $h(0)$ — the map $\theta\mapsto h(e^{i\theta})$ is a local geodesic of constant speed $\alpha$ . It is the statement that turns an analytic quantity, the order $\alpha$ , into a geometric one: the speed of a closed local geodesic in a spherical building of type $W$ . Everything that follows — pushing the curve into the model chamber $\mathbb S^{N-1}/W$ , recognizing it as a closed billiards path, lifting it to a great circle and reading off the period — is about that curve and its speed.

Note that the statement is about the angle at the cone point, not about the distance in the building. On a circle of radius $L$ the ambient distance between two points is the chord $2L|\sin(\alpha\Delta/2)|$ , strictly less than the arclength $\alpha L|\Delta|$ ; it is only in the space of directions that the parametrization has constant speed. Correspondingly, no positivity of $L$ needs to be assumed here: it follows from nonconstancy and homogeneity.

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$