In an apartment the circle of a homogeneous harmonic map solves $g''+\alpha^2 g=0$

Disproved

HarmonicBuilding.circleOscillatorInApartment

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

buildingsharmonic-mapsmetric-geometry

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 circleOscillatorInApartment
    {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) :
    ∃ delta : ℝ, 0 < delta ∧ ∀ theta0 : ℝ,
      ∃ c ∈ M.building.atlas, ∃ p0 : ModelEuclideanSpace N,
      ∃ g g' g'' : ℝ → ModelEuclideanSpace N,
        c p0 = h 0 ∧
        (∀ t : ℝ, HasDerivAt g (g' t) t) ∧
        (∀ t : ℝ, HasDerivAt g' (g'' t) t) ∧
        (∀ t : ℝ, g'' t = -(alpha ^ 2) • g t) ∧
        ∀ theta : ℝ, |theta - theta0| < delta →
          h (circlePoint 0 1 theta) = c (p0 + g theta) := by sorry

end HarmonicBuilding

Source

The apartment computation in the proof of Theorem 3.1 of C. Breiner and B. K. Dees, On the Possible Orders of Harmonic Maps into Euclidean Buildings, Calc. Var. PDE (2026), arXiv:2604.16608, together with the regularity input Theorem 2.5 quoted there; that the flat is an apartment of the atlas is Theorem 2.1 of L. Kramer, Metric properties of Euclidean buildings, arXiv:1012.2218, quoting Parreau.

View graph

In an apartment the circle of a homogeneous harmonic map solves g′′+α2g=0g''+\alpha^2 g=0g′′+α2g=0

In an apartment the circle of a homogeneous harmonic map solves $g''+\alpha^2 g=0$