Prove2Me

d2(u(eiθ),u(0))=D+Acos⁡(2αθ)+Bsin⁡(2αθ)d^2(u(e^{i\theta}),u(0)) = D + A\cos(2\alpha\theta) + B\sin(2\alpha\theta)

Disproved
HarmonicBuilding.circleDistanceSquaredForm

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

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

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 circleDistanceSquaredForm
    {N : ℕ} (C : EuclideanCoxeterData N) (M : ConicalBuildingModel.{v} N C)
    (h : ℂ → M.carrier) (alpha : ℝ)
    (hhom : IsHomogeneousOfOrderOn M Set.univ h 0 alpha)
    (hharm : IsPlanarKSHarmonicOn Set.univ h)
    (hnc : NonconstantOn h Set.univ) :
    ∃ D A B : ℝ, ∀ theta : ℝ,
      dist (h (circlePoint 0 1 theta)) (h 0) ^ 2
        = D + A * Real.cos (2 * alpha * theta)
            + B * Real.sin (2 * alpha * theta) := 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, proof of Theorem 3.1 (Section 3), steps 1 to 4: Theorem 2.5 confines singularities to the origin, the harmonic map equation in polar coordinates for u(r,theta) = r^alpha g(theta) reduces to g'' + alpha^2 g = 0, whose solution is g(theta) = v1 cos(alpha theta) + v2 sin(alpha theta), and q(theta) = d^2(u(e^{i theta}), u(0)) is the squared norm of that.

View graph