Lemma 3.2 — $\ell(u(\mathbb{S}^1)) = 2\pi\alpha L$ in the constant-distance case

Disproved

HarmonicBuilding.constantDistanceCircleLength

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

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

Throughout, $W$ is the finite Weyl group of a Euclidean Coxeter datum on an $N$ -dimensional model apartment, and a conical Euclidean building of type $W$ is a complete Euclidean building carrying a metric cone structure with cone point $0_X$ . A map $h$ of the plane into such a building is homogeneous of order $\alpha$ about $x_0$ when $h(x_0)=0_X$ and

h(x_0+\lambda z)=\lambda^{\alpha}\,h(x_0+z)\qquad\text{for all }\lambda>0,

the right side denoting dilation about the cone point.

This is the length computation in the constant-distance case. Suppose $h$ is homogeneous of order $\alpha$ and the distance to the cone point is constant along the unit circle,

d_X\bigl(h(e^{i\theta}),\,h(0)\bigr)=L \qquad\text{for all }\theta .

Then the image of the unit circle has length

\ell\bigl(h(\mathbb{S}^1)\bigr)=2\pi\,\alpha\,L .

The identity is what converts homogeneity into a statement about speed: the image curve lies on the metric sphere of radius $L$ about the cone point, and it traverses that sphere at constant speed $\alpha L$ rather than $L$ . The factor $\alpha$ is exactly the discrepancy that the subsequent billiards argument exploits, since a closed curve on a spherical building has constrained length.

Formalization Note. The length is the total variation of $\theta \mapsto h(e^{i\theta})$ over one full turn $[0,2\pi]$ , taken in the extended nonnegative reals, which is the standard metric-space notion of the length of a parametrized curve.

Preamble

import Definitions.Def_frame_2026_harmonic_building_conical

Formal statement

namespace HarmonicBuilding

open scoped Manifold

universe v w

theorem constantDistanceCircleLength
    {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) :
    unitCircleImageLength h = ENNReal.ofReal (2 * Real.pi * alpha * L) := 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, Lemma 3.2 (Section 3).

View graph

Lemma 3.2 — ℓ(u(S1))=2παL\ell(u(\mathbb{S}^1)) = 2\pi\alpha Lℓ(u(S1))=2παL in the constant-distance case

Lemma 3.2 — $\ell(u(\mathbb{S}^1)) = 2\pi\alpha L$ in the constant-distance case