Lemma 2.14 — the order is realized by a homogeneous map into a conical building

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Proved status carries no information about that problem. Do not import this node or use it as a dependency.

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 tangent-map reduction. Let $S$ be a domain in a Riemann surface, $X$ a Euclidean building of type $W$, and $u:S\to X$ a nonconstant Korevaar–Schoen harmonic map whose order at a point $x_0$ equals $\alpha$. The assertion is that there exist a conical Euclidean building $X'$ of the same type $W$ and a nonconstant homogeneous harmonic map

$$u_*:\mathbb{R}^2 \longrightarrow X'$$

of the same order $\alpha$ about the origin.

The mechanism is blow-up: rescaling $u$ around $x_0$ at a sequence of shrinking radii, with the target rescaled correspondingly, produces in the limit a map into the tangent cone at $u(x_0)$. Two facts make the statement useful. Rescaling does not change the order, so $u_*$ inherits $\alpha$ exactly; and the tangent cone of a Euclidean building of type $W$ is again a Euclidean building of type $W$, so the Coxeter data — and in particular the number $|W|$ that the final arithmetic conclusion refers to — is unchanged.

The effect of this reduction is to replace an arbitrary harmonic map on a Riemann surface by a scale-invariant model on the plane. Everything after it is a statement about homogeneous maps.

Formalization Note. The source states the conclusion for a map on the unit ball $B_1(0)\subset\mathbb{R}^2$. The statement here asks for the homogeneous model on the whole plane, which is the setting of Definition 2.13 itself and is equivalent: a map homogeneous of order $\alpha$ on a ball about the origin extends canonically to the plane by its own scaling relation, and energy minimization is scale invariant.

Why this node was retired

The posted statement is

namespace HarmonicBuilding

open scoped Manifold

universe v w

theorem orderReducesToHomogeneous
    {N : ℕ} (C : EuclideanCoxeterData N)
    {X : Type v} {S : Type w}
    [MetricSpace X] [CompleteSpace X] [MeasurableSpace X] [BorelSpace X]
    [TopologicalSpace S] [T2Space S] [SecondCountableTopology S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    (B : EuclideanBuildingData N C X)
    (D : RiemannSurfaceDomain S) (u : S → X) (x₀ : D.Point)
    (hu : IsKSHarmonic D u) (hnc : NonconstantOn u D.carrier)
    (alpha : ℝ) (halpha : HasOrderAt D u x₀ alpha) :
    ∃ M : ConicalBuildingModel.{v} N C, ∃ h : ℂ → M.carrier,
      IsHomogeneousOfOrderOn M Set.univ h 0 alpha ∧
        IsPlanarKSHarmonicOn Set.univ h ∧
        NonconstantOn h Set.univ := by sorry

end HarmonicBuilding

The energy-only harmonic predicate allows a map zero almost everywhere but pointwise nonconstant, and the output is not linked to a blow-up of the input map.

A proof of a malformed proposition can be a correct proof of that proposition, so this is not a judgment on the accepted submission — but the Proved status must not be read as settling the problem shown above.

Proposed corrected statement

Require the continuous representative of the KS-harmonic map, pointwise/essential nonconstancy consistent with that representative, and explicitly require the output target to be the tangent cone at u(z) and h to arise as a normalized blow-up limit of u at z with the same frequency/order. Do not merely existentially quantify an unrelated conical building and map.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.

import Definitions.Def_frame_2026_harmonic_building_conical

namespace HarmonicBuilding

open scoped Manifold

universe v w

theorem orderReducesToHomogeneous
    {N : ℕ} (C : EuclideanCoxeterData N)
    {X : Type v} {S : Type w}
    [MetricSpace X] [CompleteSpace X] [MeasurableSpace X] [BorelSpace X]
    [TopologicalSpace S] [T2Space S] [SecondCountableTopology S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    (B : EuclideanBuildingData N C X)
    (D : RiemannSurfaceDomain S) (u : S → X) (x₀ : D.Point)
    (hu : IsKSHarmonic D u) (hnc : NonconstantOn u D.carrier)
    (alpha : ℝ) (halpha : HasOrderAt D u x₀ alpha) :
    ∃ M : ConicalBuildingModel.{v} N C, ∃ h : ℂ → M.carrier,
      IsHomogeneousOfOrderOn M Set.univ h 0 alpha ∧
        IsPlanarKSHarmonicOn Set.univ h ∧
        NonconstantOn h Set.univ := by sorry

end HarmonicBuilding