In an apartment the map is $r^\alpha g(\theta)$ and harmonic in polar coordinates

Disproved

HarmonicBuilding.circlePolarHarmonic

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

elliptic-pdeeuclidean-buildingsharmonic-mapshomogeneous-maps

Let $M$ be a conical Euclidean building of dimension $N$ and $h:\mathbb C\to M$ a nonconstant homogeneous harmonic map of order $\alpha$ about $0$ . Then there is a $\delta>0$ such that around every $\theta_0$ the image of the unit circle lies in a single apartment, in which the map is radially homogeneous and harmonic in the ordinary sense: there are an isometric chart $\iota:\mathbb R^N\to M$ with $\iota(0)=h(0)$ and a twice differentiable angular profile $g:\mathbb R\to\mathbb R^N$ such that

w(r,\theta)=r^{\alpha}g(\theta)\quad\text{satisfies}\quad \frac{\partial^2 w}{\partial r^2}+\frac1r\frac{\partial w}{\partial r}+\frac1{r^2}\frac{\partial^2 w}{\partial\theta^2}=0\ \ (r>0),

and $h(e^{i\theta})=\iota(g(\theta))$ for $|\theta-\theta_0|<\delta$ .

Role. This is the whole geometric and analytic input to the study of the circle, and it is exactly two facts. First, regularity: homogeneity together with the regularity theorem for harmonic maps into Euclidean buildings confines the singular set of $h$ to the origin, so every point of the unit circle has a neighbourhood whose image lies in one apartment; apartments are isometric copies of $\mathbb R^N$ , and fixing coordinates so that the cone point is the origin makes the map radially homogeneous of degree $\alpha$ in those coordinates. Second, the equation: on such a neighbourhood $h$ is a regular harmonic map into a Euclidean space, hence componentwise harmonic, which in polar coordinates is the displayed identity.

Nothing is asked here beyond those two facts. The passage from this equation to a closed form is separate and already machine-checked: substituting the homogeneous form leaves the harmonic oscillator equation $g''+\alpha^2g=0$ , whose solutions are $\mathbf v_1\cos(\alpha\theta)+\mathbf v_2\sin(\alpha\theta)$ , and from there the squared distance to the cone point, the chord law on a circle of constant radius, and the angular speed all follow with no further geometry.

Formalization Note. The partial derivatives are supplied as explicit functions with hypotheses identifying them, so the harmonicity assumption is literally the displayed polar equation. The profile $g$ is asked for on all of $\mathbb R$ rather than only on the window; this is no strengthening, since the equation determines $g$ off the window by the same closed formula, and the agreement with $h$ is asserted only where the geometry holds.

Preamble

import Definitions.Def_frame_2026_harmonic_building_conical

Formal statement

namespace HarmonicBuilding

universe v

theorem circlePolarHarmonic
    {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 : ℝ,
      ∃ (iota : ModelEuclideanSpace N → M.carrier)
        (g g' g'' : ℝ → ModelEuclideanSpace N)
        (wr wrr wt wtt : ℝ → ℝ → ModelEuclideanSpace N),
        Isometry iota ∧ iota 0 = h 0 ∧
        (∀ t, HasDerivAt g (g' t) t) ∧
        (∀ t, HasDerivAt g' (g'' t) t) ∧
        (∀ r : ℝ, 0 < r → ∀ t : ℝ,
          HasDerivAt (fun s : ℝ => s ^ alpha • g t) (wr r t) r) ∧
        (∀ r : ℝ, 0 < r → ∀ t : ℝ,
          HasDerivAt (fun s : ℝ => wr s t) (wrr r t) r) ∧
        (∀ r t : ℝ, HasDerivAt (fun u : ℝ => r ^ alpha • g u) (wt r t) t) ∧
        (∀ r t : ℝ, HasDerivAt (fun u : ℝ => wt r u) (wtt r t) t) ∧
        (∀ r : ℝ, 0 < r → ∀ t : ℝ,
          wrr r t + r⁻¹ • wr r t + (r ^ 2)⁻¹ • wtt r t = 0) ∧
        (∀ theta : ℝ, |theta - theta0| < delta →
          h (circlePoint 0 1 theta) = iota (g theta)) := by sorry

end HarmonicBuilding

Source

The regularity input Theorem 2.5 and the polar-coordinate harmonic map equation displayed 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.

View graph

In an apartment the map is rαg(θ)r^\alpha g(\theta)rαg(θ) and harmonic in polar coordinates

In an apartment the map is $r^\alpha g(\theta)$ and harmonic in polar coordinates