The chord law on the circle of a homogeneous map at constant distance

Disproved

HarmonicBuilding.circleChordLaw

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

euclidean-buildingsharmonic-mapshomogeneous-mapsmetric-geometry

Let $M$ be a conical Euclidean building of type $W$ , and let $h:\mathbb C\to M$ be 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 all $\theta_1,\theta_2$ with $|\theta_1-\theta_2|\le\delta$ ,

d\bigl(h(e^{i\theta_1}),\,h(e^{i\theta_2})\bigr)=2L\left|\sin\frac{\alpha(\theta_1-\theta_2)}{2}\right| .

Role. Homogeneity and the fact that the singular set of a homogeneous harmonic map from a surface is contained in the origin put every point of the unit circle in the interior of a region on which $h$ takes values in a single apartment $A$ . Working in $A$ with the cone point at the origin, the harmonic map equation in polar coordinates forces the representation

h(r,\theta)=r^{\alpha}\bigl(\cos(\alpha\theta)\,\mathbf v_1+\sin(\alpha\theta)\,\mathbf v_2\bigr),

and the constant-distance hypothesis forces $\mathbf v_1,\mathbf v_2$ to be orthogonal of common length $L$ . The displayed identity is then the Euclidean chord of the circle of radius $L$ traversed at angular rate $\alpha$ , read in the apartment; since apartments are isometrically embedded, it is an identity in $M$ .

This is the local form from which the two global facts about the circle follow. The comparison angle at the cone point between two nearby points of the circle is $\alpha|\theta_1-\theta_2|$ , so that after rescaling into the space of directions the circle is a local geodesic of speed $\alpha$ ; and the length of the circle's image is $2\pi\alpha L$ , since the chord law makes each short arc isometric to a Euclidean circular arc.

Formalization Note. This statement replaces an earlier and incorrect one asserting $d(h(e^{i\theta_1}),h(e^{i\theta_2}))=\alpha L|\theta_1-\theta_2|$ on small intervals. That identity equates a chord with an arclength and is false for every nondegenerate configuration: on the circle of radius $L$ the chord $2L|\sin(\alpha\Delta/2)|$ is strictly smaller than the arclength $\alpha L|\Delta|$ whenever $\alpha L\Delta\ne0$ . The constant-speed statement of the source is about the space of directions, whose metric is the angle at the cone point, not about the metric of the building.

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 circleChordLaw
    {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 →
      dist (h (circlePoint 0 1 theta1)) (h (circlePoint 0 1 theta2))
        = 2 * L * |Real.sin (alpha * (theta1 - theta2) / 2)| := 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