Constant distance forces the apartment frame to be orthonormal of radius L

Disproved

HarmonicBuilding.frame_orthonormal_of_constantDistance

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

euclidean-buildingsharmonic-mapsmetric-geometryspherical-geometry

Let $h$ be a nonconstant homogeneous energy minimizer of order $\alpha\neq0$ into a conical Euclidean building whose distance to the cone point along the unit circle is the constant $L$ . Then locally the circle image is a genuine circle of radius $L$ in an apartment: there is $\delta>0$ such that around each $\theta_0$ one finds an isometric embedding $\iota$ of the model apartment with $\iota(0)=h(0)$ and an orthonormal pair $v_1,v_2$ with

h\bigl(e^{i\theta}\bigr)=\iota\bigl(L\,\gamma_{v_1,v_2}(\alpha\theta)\bigr),\qquad|\theta-\theta_0|<\delta .

Role. Local flatness alone produces some frame $a,b$ spanning the arc, with no control on its shape. The constant-distance hypothesis — the branch of the order dichotomy in which the circle image lies on a sphere about the cone point — pins that frame down completely: it must be orthogonal with both vectors of length $L$ . This is what turns the flatness statement into the input the closed-billiards-path analysis needs, since that analysis is phrased in terms of an orthonormal pair spanning a great circle.

Proof. The constant $L$ is positive, since otherwise homogeneity would make $h$ constant. Local flatness supplies $\iota$ and vectors $a,b$ with $h(e^{i\theta})=\iota(\cos(\alpha\theta)a+\sin(\alpha\theta)b)$ on a short arc. As $\iota$ is an isometry fixing the cone point, the squared distance to the cone point is $\|\cos(\alpha\theta)a+\sin(\alpha\theta)b\|^{2}$ , which expands by the double-angle identities to

\frac{\|a\|^{2}+\|b\|^{2}}{2}+\frac{\|a\|^{2}-\|b\|^{2}}{2}\cos(2\alpha\theta)+\langle a,b\rangle\sin(2\alpha\theta).

The hypothesis says this equals $L^{2}$ throughout the arc, so a single-frequency trigonometric polynomial is constant there; since $\alpha\neq0$ , all of its coefficients vanish. Hence $\|a\|=\|b\|$ , $\langle a,b\rangle=0$ and $\|a\|^{2}=L^{2}$ , so $v_1=a/L$ and $v_2=b/L$ are orthonormal and $\cos(\alpha\theta)a+\sin(\alpha\theta)b=L\,\gamma_{v_1,v_2}(\alpha\theta)$ .

Preamble

import Definitions.Def_frame_2026_harmonic_building_conical
import Definitions.Def_spherical_great_circle

Formal statement

namespace HarmonicBuilding

open SphericalGeometry

universe v

theorem frame_orthonormal_of_constantDistance
    {N : ℕ} (C : EuclideanCoxeterData N) (M : ConicalBuildingModel.{v} N C)
    (h : ℂ → M.carrier) (alpha L : ℝ) (halpha : alpha ≠ 0)
    (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 ∧ ∀ theta0 : ℝ,
      ∃ (iota : ModelEuclideanSpace N → M.carrier)
        (v1 v2 : ModelEuclideanSpace N),
        Isometry iota ∧ iota 0 = h 0 ∧
        ‖v1‖ = 1 ∧ ‖v2‖ = 1 ∧ inner ℝ v1 v2 = (0:ℝ) ∧
        ∀ theta : ℝ, |theta - theta0| < delta →
          h (circlePoint 0 1 theta)
            = iota (L • greatCirclePath v1 v2 (alpha * theta)) := by sorry

end HarmonicBuilding

Source

The constant-distance branch of the order dichotomy in Section 3 of C. Breiner and B. K. Dees, On the Possible Orders of Harmonic Maps into Euclidean Buildings, Calc. Var. PDE (2026), arXiv:2604.16608.

View graph