Euclidean-building harmonic-map order interfaces

Definition

frame_2026_harmonic_building_interfaces

by ShouqiaoWang · Aug 26, 2026 · Mathlib c5ea003 (Lean v4.30.0)

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

This definition bundle fixes the geometric and analytic objects needed to state the order-classification theorem for harmonic maps into Euclidean buildings. It defines an $N$ -dimensional Euclidean Coxeter datum from a finite affine reflection group and its finite rotational image $W$ , a complete metric Euclidean building equipped with a maximal compatible apartment atlas, and a connected open domain in a complex one-dimensional manifold. It then gives concrete Korevaar--Schoen-style local energy, Sobolev, trace, boundary-moment, frequency, harmonic-minimization, and order predicates. The main proposition PossibleOrdersProblem requires a nonconstant harmonic map and concludes that the order is defined, equals $m/k$ with positive integers $m,k$ and $k\mid |W|$ , and in rank one equals $m/2$ for some $m\ge2$ . The analytic quantities are determined by the geometry rather than passed in as arbitrary semantic predicates.

Definition code

import Mathlib

/-!
# Canonical foundations for harmonic maps into Euclidean buildings

The definitions in this file contain no user-supplied Sobolev predicate,
energy density, volume measure, boundary measure, or frequency function.
The source is a one-dimensional complex manifold, the Coxeter groups act by
concrete affine/linear isometries, and the analytic quantities are fixed by a
normalized Korevaar--Schoen difference-quotient construction in complex
coordinates.

The normalization `4 / (pi * epsilon^4)` is the two-dimensional normalization:
for a smooth Euclidean-valued map the approximate density converges to the
usual squared Hilbert--Schmidt norm of its derivative.
-/

namespace HarmonicBuilding

open MeasureTheory
open scoped ENNReal Manifold

/-! ## Riemann surfaces -/

/-- A domain in a Riemann surface.  The ambient instances say that `S` is a
Hausdorff, second-countable, one-complex-dimensional smooth manifold. -/
structure RiemannSurfaceDomain (S : Type*) [TopologicalSpace S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S] where
  carrier : Set S
  isOpen_carrier : IsOpen carrier
  isConnected_carrier : IsConnected carrier

/-- Points of a Riemann-surface domain. -/
abbrev RiemannSurfaceDomain.Point {S : Type*} [TopologicalSpace S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    (D : RiemannSurfaceDomain S) := D.carrier

/-- The whole complex plane is an explicit inhabited example of the source
geometry; the domain interface is therefore not empty by construction. -/
def complexPlaneDomain : RiemannSurfaceDomain ℂ where
  carrier := Set.univ
  isOpen_carrier := isOpen_univ
  isConnected_carrier := isConnected_univ

/-- A map is genuinely nonconstant on the specified domain. -/
def NonconstantOn {S X : Type*} (u : S → X) (D : Set S) : Prop :=
  ∃ x ∈ D, ∃ y ∈ D, u x ≠ u y

/-! ## Concrete Euclidean Coxeter data -/

/-- The model apartment `E^N`. -/
abbrev ModelEuclideanSpace (N : ℕ) := EuclideanSpace ℝ (Fin N)

/-- The full group of affine isometries of the model apartment. -/
abbrev EuclideanIsometryGroup (N : ℕ) :=
  ModelEuclideanSpace N ≃ᵃⁱ[ℝ] ModelEuclideanSpace N

/-- The full orthogonal group of the translation vector space. -/
abbrev OrthogonalGroup (N : ℕ) :=
  ModelEuclideanSpace N ≃ₗᵢ[ℝ] ModelEuclideanSpace N

/-- A linear isometry is reflection in the hyperplane perpendicular to a
nonzero normal vector. -/
def IsLinearReflection {N : ℕ} (g : OrthogonalGroup N) : Prop :=
  ∃ n : ModelEuclideanSpace N, n ≠ 0 ∧
    ∀ x : ModelEuclideanSpace N,
      g x = x - (2 * (inner ℝ x n / inner ℝ n n)) • n

/-- An affine isometry is a reflection when it has a fixed point and its
linear part is a hyperplane reflection. -/
def IsAffineReflection {N : ℕ} (g : EuclideanIsometryGroup N) : Prop :=
  (∃ p : ModelEuclideanSpace N, g p = p) ∧
    IsLinearReflection g.linearIsometryEquiv

/-- A Euclidean Coxeter complex represented inside the actual affine and
orthogonal isometry groups of `E^N`.  Surjectivity together with
`rotationalPart_value` makes `weyl` exactly the rotational image; it cannot be
an unrelated finite group.  The affine group is required to be generated by a
nonempty set of genuine affine reflections. -/
structure EuclideanCoxeterData (N : ℕ) where
  positive_rank : 0 < N
  affineWeyl : Subgroup (EuclideanIsometryGroup N)
  weyl : Subgroup (OrthogonalGroup N)
  instFintypeWeyl : Fintype weyl
  rotationalPart : affineWeyl →* weyl
  rotationalPart_value : ∀ g : affineWeyl,
    ((rotationalPart g : weyl) : OrthogonalGroup N) =
      (g : EuclideanIsometryGroup N).linearIsometryEquiv
  rotationalPart_surjective : Function.Surjective rotationalPart
  simpleReflections : Set affineWeyl
  simpleReflections_nonempty : simpleReflections.Nonempty
  simple_are_affine_reflections : ∀ g ∈ simpleReflections,
    IsAffineReflection (g : EuclideanIsometryGroup N)
  simple_generates : Subgroup.closure simpleReflections = ⊤

attribute [instance] EuclideanCoxeterData.instFintypeWeyl

/-! ## Metric Euclidean buildings -/

/-- An apartment chart is an isometric embedding of the model apartment. -/
structure ApartmentChart (E X : Type*) [PseudoMetricSpace E]
    [PseudoMetricSpace X] where
  toFun : E → X
  isometry : Isometry toFun

instance {E X : Type*} [PseudoMetricSpace E] [PseudoMetricSpace X] :
    CoeFun (ApartmentChart E X) (fun _ ↦ E → X) :=
  ⟨ApartmentChart.toFun⟩

/-- A unit-interval constant-speed geodesic segment. -/
def IsConstantSpeedSegment {X : Type*} [PseudoMetricSpace X]
    (gamma : ℝ → X) (x y : X) : Prop :=
  gamma 0 = x ∧ gamma 1 = y ∧
    ∀ s ∈ Set.Icc (0 : ℝ) 1, ∀ t ∈ Set.Icc (0 : ℝ) 1,
      dist (gamma s) (gamma t) = |s - t| * dist x y

/-- An isometrically parametrized geodesic line. -/
def IsGeodesicLine {X : Type*} [PseudoMetricSpace X] (gamma : ℝ → X) : Prop :=
  ∀ s t : ℝ, dist (gamma s) (gamma t) = |s - t|

/-- An isometrically parametrized geodesic ray on nonnegative times. -/
def IsGeodesicRay {X : Type*} [PseudoMetricSpace X] (gamma : ℝ → X) : Prop :=
  ∀ s t : ℝ, 0 ≤ s → 0 ≤ t →
    dist (gamma s) (gamma t) = |s - t|

/-- The CAT(0) CN inequality, together with geodesic existence. -/
def IsCATZero (X : Type*) [PseudoMetricSpace X] : Prop :=
  (∀ x y : X, ∃ gamma : ℝ → X, IsConstantSpeedSegment gamma x y) ∧
  ∀ x y z : X, ∀ gamma : ℝ → X,
    IsConstantSpeedSegment gamma x y →
      ∀ t ∈ Set.Icc (0 : ℝ) 1,
        dist (gamma t) z ^ 2 ≤
          (1 - t) * dist x z ^ 2 + t * dist y z ^ 2 -
            t * (1 - t) * dist x y ^ 2

/-- Two apartment charts have a transition map in the concrete affine Weyl
group on their entire overlap. -/
def ChartsCompatible {n : ℕ} {X : Type*} [PseudoMetricSpace X]
    (C : EuclideanCoxeterData n)
    (c₁ c₂ : ApartmentChart (ModelEuclideanSpace n) X) : Prop :=
  ∃ w : C.affineWeyl, ∀ p q : ModelEuclideanSpace n,
    c₁ p = c₂ q → (w : EuclideanIsometryGroup n) q = p

/-- A Kleiner--Leeb style metric Euclidean building realization.  Besides
CAT(0), pair coverage and Weyl-compatible overlaps, rays and lines lie in
apartments and the atlas is maximal among compatible charts. -/
structure EuclideanBuildingData (N : ℕ) (C : EuclideanCoxeterData N)
    (X : Type*) [MetricSpace X] [CompleteSpace X] where
  atlas : Set (ApartmentChart (ModelEuclideanSpace N) X)
  pair_mem_apartment : ∀ x y : X,
    ∃ chart ∈ atlas, x ∈ Set.range chart.toFun ∧ y ∈ Set.range chart.toFun
  ray_mem_apartment : ∀ gamma : ℝ → X, IsGeodesicRay gamma →
    ∃ chart ∈ atlas,
      gamma '' Set.Ici (0 : ℝ) ⊆ Set.range chart.toFun
  line_mem_apartment : ∀ gamma : ℝ → X, IsGeodesicLine gamma →
    ∃ chart ∈ atlas, Set.range gamma ⊆ Set.range chart.toFun
  overlap_compatible : ∀ c₁ ∈ atlas, ∀ c₂ ∈ atlas,
    ChartsCompatible C c₁ c₂
  maximal_atlas : ∀ c : ApartmentChart (ModelEuclideanSpace N) X,
    (∀ a ∈ atlas, ChartsCompatible C c a) → c ∈ atlas
  catZeroComparison : IsCATZero X

/-! ## Canonical two-dimensional Korevaar--Schoen energy -/

/-- The normalized two-dimensional metric difference-quotient density. -/
noncomputable def ksApproxEnergyDensity {X : Type*} [PseudoMetricSpace X]
    (Omega : Set ℂ) (u : ℂ → X) (epsilon : ℝ) (z : ℂ) : ENNReal :=
  ENNReal.ofReal (4 / (Real.pi * epsilon ^ 4)) *
    ∫⁻ w in Omega ∩ Metric.ball z epsilon,
      ENNReal.ofReal (dist (u w) (u z) ^ 2)

/-- Approximate energy on `U`, using the fixed Lebesgue area on `ℂ`. -/
noncomputable def ksApproxEnergy {X : Type*} [PseudoMetricSpace X]
    (Omega U : Set ℂ) (u : ℂ → X) (epsilon : ℝ) : ENNReal :=
  ∫⁻ z in U ∩ Omega,
    ksApproxEnergyDensity (U ∩ Omega) u epsilon z

/-- The Korevaar--Schoen energy is the lower small-scale envelope of the
normalized approximate energies. -/
noncomputable def ksEnergy {X : Type*} [PseudoMetricSpace X]
    (Omega U : Set ℂ) (u : ℂ → X) : ENNReal :=
  Filter.liminf (fun epsilon : ℝ ↦ ksApproxEnergy Omega U u epsilon)
    (nhdsWithin 0 (Set.Ioi 0))

/-- Canonical local metric `W^{1,2}` membership: Borel measurability on the
coordinate domain, metric-valued `L²` integrability, and finite normalized KS
energy on `U`.  The existential point is only the standard base point used to
define metric-valued `L²`; changing it does not change the condition. -/
def IsKSSobolevOn {X : Type*} [PseudoMetricSpace X] [MeasurableSpace X]
    (Omega U : Set ℂ) (u : ℂ → X) : Prop :=
  AEMeasurable u (volume.restrict Omega) ∧
    (∃ q : X,
      (∫⁻ z in U ∩ Omega, ENNReal.ofReal (dist (u z) q ^ 2)) < ⊤) ∧
    ksEnergy Omega U u < ⊤

/-- The standard angular parametrization of a Euclidean coordinate circle. -/
noncomputable def circlePoint (z : ℂ) (r theta : ℝ) : ℂ :=
  z + (r : ℂ) * Complex.exp ((theta : ℂ) * Complex.I)

/-- Normalized squared distance in an interior collar of a circle.  Unlike a
pointwise restriction, this is unchanged by altering Sobolev representatives
on an area-null set. -/
noncomputable def annularTraceDistance {X : Type*} [PseudoMetricSpace X]
    (u v : ℂ → X) (z : ℂ) (R delta : ℝ) : ENNReal :=
  ENNReal.ofReal (1 / delta) *
    ∫⁻ w in {w : ℂ | R - delta < dist w z ∧ dist w z < R},
      ENNReal.ofReal (dist (u w) (v w) ^ 2)

/-- Equality of Sobolev traces on a coordinate circle, defined canonically by
vanishing normalized `L²` distance in shrinking interior collars. -/
def SameKSTraceOnCircle {X : Type*} [PseudoMetricSpace X]
    (u v : ℂ → X) (z : ℂ) (R : ℝ) : Prop :=
  Filter.Tendsto (fun delta : ℝ ↦ annularTraceDistance u v z R delta)
    (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

/-- Energy minimization on one relatively compact coordinate ball. -/
def IsPlanarKSHarmonicAt {X : Type*} [PseudoMetricSpace X]
    [MeasurableSpace X] (Omega : Set ℂ) (u : ℂ → X) (z : ℂ) : Prop :=
  z ∈ Omega ∧ ∃ R : ℝ, 0 < R ∧ Metric.closedBall z R ⊆ Omega ∧
    IsKSSobolevOn Omega (Metric.ball z R) u ∧
    ∀ v : ℂ → X,
      IsKSSobolevOn Omega (Metric.ball z R) v →
      SameKSTraceOnCircle u v z R →
      ksEnergy Omega (Metric.ball z R) u ≤
        ksEnergy Omega (Metric.ball z R) v

/-! ## Pullback to canonical complex coordinates -/

/-- The part of a Riemann-surface domain seen in the preferred extended chart
at `x`. -/
noncomputable def coordinateDomainAt {S : Type*} [TopologicalSpace S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    (D : RiemannSurfaceDomain S) (x : S) : Set ℂ :=
  extChartAt (modelWithCornersSelf ℂ ℂ) x ''
    (D.carrier ∩ (extChartAt (modelWithCornersSelf ℂ ℂ) x).source)

/-- A map written in the preferred complex chart at `x`. -/
noncomputable def coordinateMapAt {S X : Type*} [TopologicalSpace S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    (u : S → X) (x : S) : ℂ → X :=
  fun z ↦ u ((extChartAt (modelWithCornersSelf ℂ ℂ) x).symm z)

/-- The coordinate of the distinguished surface point. -/
noncomputable def coordinateCenter {S : Type*} [TopologicalSpace S]
    [ChartedSpace ℂ S] (x : S) : ℂ :=
  extChartAt (modelWithCornersSelf ℂ ℂ) x x

/-- A KS-energy-minimizing harmonic map on a Riemann-surface domain.  The
quantification over every point makes this independent of any caller-selected
energy or Sobolev predicate. -/
def IsKSHarmonic {S X : Type*} [TopologicalSpace S] [ChartedSpace ℂ S]
    [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    [PseudoMetricSpace X] [MeasurableSpace X]
    (D : RiemannSurfaceDomain S) (u : S → X) : Prop :=
  ContinuousOn u D.carrier ∧
    ∀ x ∈ D.carrier,
      IsPlanarKSHarmonicAt (coordinateDomainAt D x) (coordinateMapAt u x)
        (coordinateCenter x)

/-- Canonical boundary moment, with the factor `r` giving arclength measure. -/
noncomputable def boundaryMoment {X : Type*} [PseudoMetricSpace X]
    (u : ℂ → X) (z : ℂ) (r : ℝ) : ENNReal :=
  ENNReal.ofReal r *
    ∫⁻ theta in Set.Icc (0 : ℝ) (2 * Real.pi),
      ENNReal.ofReal
        (dist (u (circlePoint z r theta)) (u z) ^ 2)

/-- Scale energy on a coordinate ball, converted to a real after finiteness. -/
noncomputable def scaleEnergy {X : Type*} [PseudoMetricSpace X]
    (Omega : Set ℂ) (u : ℂ → X) (z : ℂ) (r : ℝ) : ℝ :=
  (ksEnergy Omega (Metric.ball z r) u).toReal

/-- The canonical frequency quotient `r E_u(z,r) / I_u(z,r)`. -/
noncomputable def frequencyQuotient {X : Type*} [PseudoMetricSpace X]
    (Omega : Set ℂ) (u : ℂ → X) (z : ℂ) (r : ℝ) : ℝ :=
  r * scaleEnergy Omega u z r / (boundaryMoment u z r).toReal

/-- The surface frequency in the preferred complex coordinate at `x`. -/
noncomputable def surfaceFrequency {S X : Type*} [TopologicalSpace S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    [PseudoMetricSpace X] (D : RiemannSurfaceDomain S) (u : S → X)
    (x : S) (r : ℝ) : ℝ :=
  frequencyQuotient (coordinateDomainAt D x) (coordinateMapAt u x)
    (coordinateCenter x) r

/-- The order of `u` at `x` is `alpha` precisely when the canonical frequency
has that limit through positive radii. -/
def HasOrderAt {S X : Type*} [TopologicalSpace S] [ChartedSpace ℂ S]
    [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    [PseudoMetricSpace X] (D : RiemannSurfaceDomain S) (u : S → X)
    (x : S) (alpha : ℝ) : Prop :=
  Filter.Tendsto (surfaceFrequency D u x)
    (nhdsWithin 0 (Set.Ioi 0)) (nhds alpha)

/-- At sufficiently small positive scales the coordinate ball stays in the
domain, its KS energy is finite, and the canonical circle moment is positive.
This is a conclusion to be proved for nonconstant harmonic maps, not an input
energy-interface hypothesis. -/
def OrderDefinedAt {S X : Type*} [TopologicalSpace S] [ChartedSpace ℂ S]
    [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    [PseudoMetricSpace X] (D : RiemannSurfaceDomain S) (u : S → X)
    (x : S) : Prop :=
  ∃ r₀ : ℝ, 0 < r₀ ∧ ∀ r : ℝ, 0 < r → r < r₀ →
    Metric.closedBall (coordinateCenter x) r ⊆ coordinateDomainAt D x ∧
    ksEnergy (coordinateDomainAt D x) (Metric.ball (coordinateCenter x) r)
      (coordinateMapAt u x) < ⊤ ∧
    0 < (boundaryMoment (coordinateMapAt u x) (coordinateCenter x) r).toReal

/-- Rank one means apartment dimension one. -/
def IsRankOne (N : ℕ) : Prop := N = 1

/-- The complete source proposition, separated from the open theorem so it can
be published first as a Prove2me definition item.  The paper's tangent-map
reduction is stated for nonconstant maps; this hypothesis is made explicit so
that the constant-map `0 / 0` frequency is not silently assigned an order.
The existence of the order and positivity of its small-scale denominator are
part of the conclusion, rather than assumptions supplied to the solver. -/
def PossibleOrdersProblem
    {N : ℕ} (C : EuclideanCoxeterData N)
    {X S : Type*}
    [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) : Prop :=
  IsKSHarmonic D u →
  NonconstantOn u D.carrier →
    OrderDefinedAt D u x₀ ∧
      (∃ m k : ℕ, 0 < m ∧ 0 < k ∧ k ≤ m ∧
        k ∣ Fintype.card C.weyl ∧
        HasOrderAt D u x₀ ((m : ℝ) / (k : ℝ))) ∧
      (IsRankOne N →
        ∃ m : ℕ, 2 ≤ m ∧
          HasOrderAt D u x₀ ((m : ℝ) / 2))

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), Theorem 1.1 on physical p. 2; definitions and reduction in Section 2: https://doi.org/10.1007/s00526-026-03375-5

Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

RiemannSurfaceDomain. Given a type $S$ with a topology, a complex charted-space structure, and the structure of a smooth manifold modeled on the one-dimensional complex vector space, a RiemannSurfaceDomain S consists of a subset $D\subseteq S$ together with proofs that $D$ is open and connected. Mathlib’s connectedness condition includes nonemptiness. This structure declaration itself does not assume that $S$ is Hausdorff or second countable.

RiemannSurfaceDomain.Point. For a domain $D$ , D.Point is the subtype of elements $x:S$ satisfying $x\in D$ .

complexPlaneDomain. complexPlaneDomain is the domain in $\mathbb C$ whose carrier is all of $\mathbb C$ .

NonconstantOn. For a function $u:S\to X$ and subset $D\subseteq S$ , NonconstantOn u D means that there exist $x,y\in D$ with $u(x)\ne u(y)$ . It asserts no continuity or regularity.

ModelEuclideanSpace. For $N\in\mathbb N$ , the model Euclidean space is the Euclidean vector space of real functions on $\operatorname{Fin}(N)$ , hence $\mathbb R^N$ with its standard Euclidean structure. For $N=0$ it is zero-dimensional.

EuclideanIsometryGroup. For $N\in\mathbb N$ , this is the full group of affine isometric equivalences of the model Euclidean space with itself.

OrthogonalGroup. For $N\in\mathbb N$ , this is the full group of linear isometric equivalences of the model Euclidean space with itself.

IsLinearReflection. For an orthogonal transformation $g$ of the model Euclidean space, IsLinearReflection g means that there exists a nonzero vector $n$ such that, for every vector $x$ ,

g(x)=x-\left(2\,\frac{\langle x,n\rangle}{\langle n,n\rangle}\right)n.

The same nonzero normal $n$ must work for every $x$ . In dimension zero this condition is impossible because no nonzero $n$ exists.

IsAffineReflection. For an affine isometry $g$ , IsAffineReflection g means both that $g$ has at least one fixed point and that its linear part satisfies the preceding explicit reflection formula for some nonzero normal vector.

EuclideanCoxeterData. For $N\in\mathbb N$ , an object $C$ of this structure contains: a proof that $N>0$ ; a subgroup $C_{\mathrm{aff}}$ of the full affine-isometry group of $\mathbb R^N$ ; a subgroup $W$ of the full orthogonal group; a finite-type structure on the elements of $W$ ; a group homomorphism $\rho:C_{\mathrm{aff}}\to W$ whose underlying orthogonal transformation at every $g$ is exactly the linear part of the underlying affine isometry $g$ ; a proof that $\rho$ is surjective; and a nonempty set $R\subseteq C_{\mathrm{aff}}$ such that every member of $R$ , viewed as an affine isometry, is an affine reflection in the preceding sense and the subgroup generated by $R$ is all of $C_{\mathrm{aff}}$ . The finite-type field is installed as the finite-type instance for $W$ . No discreteness, local finiteness, or faithfulness condition beyond the displayed concrete subgroup inclusions and equations is separately asserted.

ApartmentChart. For pseudometric spaces $E$ and $X$ , an apartment chart is a function $c:E\to X$ that preserves every distance. At this general pseudometric level the structure contains only the distance-preservation assertion; charts are thereafter coerced to their underlying functions.

IsConstantSpeedSegment. For a pseudometric space $X$ , a function $\gamma:\mathbb R\to X$ , and points $x,y\in X$ , this condition means $\gamma(0)=x$ , $\gamma(1)=y$ , and, for every $s,t\in[0,1]$ ,

d(\gamma(s),\gamma(t))=|s-t|\,d(x,y).

Values of $\gamma$ outside $[0,1]$ are unconstrained.

IsGeodesicLine. A function $\gamma:\mathbb R\to X$ is a geodesic line exactly when $d(\gamma(s),\gamma(t))=|s-t|$ for every real $s,t$ .

IsGeodesicRay. A function $\gamma:\mathbb R\to X$ is a geodesic ray exactly when $d(\gamma(s),\gamma(t))=|s-t|$ whenever both $s$ and $t$ are nonnegative. Its values at negative times are unconstrained.

IsCATZero. A pseudometric space $X$ satisfies this predicate when, first, every ordered pair $x,y\in X$ admits a constant-speed segment as defined above and, second, for every $x,y,z\in X$ , every function $\gamma:\mathbb R\to X$ that is such a segment from $x$ to $y$ , and every $t\in[0,1]$ ,

d(\gamma(t),z)^2\le(1-t)d(x,z)^2+t\,d(y,z)^2-t(1-t)d(x,y)^2.

Completeness is not part of this predicate. If $X$ is empty, both universal parts are vacuous.

ChartsCompatible. Given Coxeter data $C$ in dimension $n$ and two apartment charts $c_1,c_2:\mathbb R^n\to X$ , compatibility means that there exists one element $w\in C_{\mathrm{aff}}$ such that, for every $p,q\in\mathbb R^n$ ,

c_1(p)=c_2(q)\quad\Longrightarrow\quad w(q)=p.

If the chart images are disjoint, the implication is vacuous and any available $w$ , such as the identity, can witness compatibility. The definition imposes no equation on pairs whose chart images are unequal.

EuclideanBuildingData. Given $N$ , Coxeter data $C$ , and a complete metric space $X$ , this structure consists of a set $\mathcal A$ of apartment charts $\mathbb R^N\to X$ satisfying all of the following: every pair $x,y\in X$ lies in the range of a common chart in $\mathcal A$ ; the image at nonnegative times of every geodesic ray is contained in the range of some chart in $\mathcal A$ ; the entire range of every geodesic line is contained in the range of some chart in $\mathcal A$ ; every ordered pair of charts in $\mathcal A$ is compatible in the preceding single-affine-Weyl-element sense; every apartment chart compatible with every member of $\mathcal A$ already belongs to $\mathcal A$ ; and $X$ satisfies the preceding CAT(0) existence and comparison predicate. If $X$ is empty, the pair, ray, and line requirements are vacuous; since the model apartment is inhabited and there is no function from it to an empty $X$ , the empty atlas also satisfies the maximality clause.

ksApproxEnergyDensity. Given a pseudometric target $X$ , a set $\Omega\subseteq\mathbb C$ , a total function $u:\mathbb C\to X$ , a real scale $\epsilon$ , and $z\in\mathbb C$ , the approximate density is the extended nonnegative real

\operatorname{ofReal}\!\left(\frac{4}{\pi\epsilon^4}\right)\,\int_{\Omega\cap B(z,\epsilon)}\operatorname{ofReal}\!\left(d(u(w),u(z))^2\right)\,dw,

where the integral is the nonnegative Lebesgue integral on $\mathbb C$ . At $\epsilon=0$ , real division by zero yields zero in the prefactor and the open ball is empty; for $\epsilon<0$ the ball is also empty. Thus the density is zero at every nonpositive scale.

ksApproxEnergy. Given sets $\Omega,U\subseteq\mathbb C$ , a total function $u:\mathbb C\to X$ , and a real scale $\epsilon$ , the approximate energy is

\int_{U\cap\Omega}\operatorname{ksApproxEnergyDensity}(U\cap\Omega,u,\epsilon,z)\,dz.

Consequently the inner integration at $z$ ranges over $(U\cap\Omega)\cap B(z,\epsilon)$ : the density is called with $U\cap\Omega$ , not with $\Omega$ alone. This energy is zero at nonpositive $\epsilon$ .

ksEnergy. The energy of $u$ on $U$ relative to $\Omega$ is the order-theoretic lower limit, in the extended nonnegative reals, of the preceding approximate energies as $\epsilon$ tends to $0$ through positive real values. It is a liminf, not an assertion that an ordinary limit exists, and it may equal infinity.

IsKSSobolevOn. Given a pseudometric and measurable target $X$ , sets $\Omega,U\subseteq\mathbb C$ , and a total function $u:\mathbb C\to X$ , this predicate requires: $u$ is almost-everywhere measurable for Lebesgue measure restricted to all of $\Omega$ ; there exists a point $q\in X$ for which

\int_{U\cap\Omega}\operatorname{ofReal}\!\left(d(u(z),q)^2\right)\,dz<\infty;

and the preceding KS energy on $U$ relative to $\Omega$ is finite. If $U\cap\Omega$ is empty, the integral and energy conditions are automatically zero once a $q$ exists, but measurability is still required on all of $\Omega$ .

circlePoint. For $z\in\mathbb C$ and real $r,\theta$ , this is the complex number $z+r e^{i\theta}$ . Negative and zero radii are allowed by the definition.

annularTraceDistance. Given total maps $u,v:\mathbb C\to X$ , center $z$ , and real numbers $R,\delta$ , this is

\operatorname{ofReal}(1/\delta)\int_{\{w:\ R-\delta<d(w,z)<R\}}\operatorname{ofReal}\!\left(d(u(w),v(w))^2\right)\,dw.

For $\delta\le0$ , ofReal(1/δ) is zero and the displayed strict annulus is empty; for $R\le0$ the annulus is also empty because distances are nonnegative.

SameKSTraceOnCircle. Two total maps $u,v:\mathbb C\to X$ have the same trace on the circle of center $z$ and real radius $R$ exactly when their preceding annular trace distance tends to $0$ as $\delta\to0$ through positive values. For $R\le0$ , the annuli are empty and this condition holds automatically.

IsPlanarKSHarmonicAt. Given $\Omega\subseteq\mathbb C$ , a total map $u:\mathbb C\to X$ , and $z\in\mathbb C$ , this means that $z\in\Omega$ and there exists $R>0$ such that the closed ball $\overline B(z,R)$ is contained in $\Omega$ , $u$ satisfies IsKSSobolevOn with $U=B(z,R)$ , and every total competitor $v:\mathbb C\to X$ that satisfies the same Sobolev predicate and has the same shrinking-collar trace as $u$ at radius $R$ satisfies

E_{\mathrm{KS}}(\Omega,B(z,R),u)\le E_{\mathrm{KS}}(\Omega,B(z,R),v).

The Sobolev predicate requires both $u$ and each competitor to be almost-everywhere measurable on all of $\Omega$ , not only on the ball, and competitors are not required to agree with $u$ away from the trace condition.

coordinateDomainAt. Given a Riemann-surface domain $D$ and any $x\in S$ , this is the image under the preferred extended chart at $x$ of $D\cap\operatorname{source}(\operatorname{extChartAt}_x)$ .

coordinateMapAt. Given $u:S\to X$ and any $x\in S$ , this is the total function on $\mathbb C$ defined by $z\mapsto u(\operatorname{extChartAt}_x^{-1}(z))$ , using the total inverse function carried by the extended local chart even at inputs outside its chart target.

coordinateCenter. Given $x\in S$ , this is the complex coordinate $\operatorname{extChartAt}_x(x)$ .

IsKSHarmonic. Given a Riemann-surface domain $D$ and map $u:S\to X$ , this predicate requires that $u$ be continuous on $D$ and that, for every $x\in D$ , the total coordinate expression of $u$ at $x$ be planar KS-harmonic at the coordinate of $x$ relative to the coordinate image of $D$ at $x$ , with all terms interpreted by the preceding definitions.

boundaryMoment. Given a total map $u:\mathbb C\to X$ , center $z$ , and real radius $r$ , the boundary moment is the extended nonnegative real

\operatorname{ofReal}(r)\int_0^{2\pi}\operatorname{ofReal}\!\left(d(u(z+r e^{i\theta}),u(z))^2\right)\,d\theta.

For $r\le0$ , the ofReal(r) factor is zero, so the boundary moment is zero.

scaleEnergy. Given $\Omega,u,z,r$ , this is the real number obtained by applying the extended-nonnegative-real toReal operation to the KS energy on the open ball $B(z,r)$ . Finite energies are converted to their real values, but infinite energy is converted to $0$ .

frequencyQuotient. The frequency quotient is the total real-valued expression

\frac{r\,\operatorname{scaleEnergy}(\Omega,u,z,r)}{\operatorname{toReal}(\operatorname{boundaryMoment}(u,z,r))}.

Real division by a zero denominator is defined to be zero. Thus the quotient is still defined, and equals zero, when the converted boundary moment is zero; infinite KS energy also contributes scale energy zero because of toReal.

surfaceFrequency. Given $D,u,x,r$ , the surface frequency is the preceding quotient computed from the coordinate domain at $x$ , the total coordinate expression of $u$ at $x$ , and the coordinate center of $x$ .

HasOrderAt. The map $u$ has order $\alpha\in\mathbb R$ at $x$ exactly when its surface-frequency function tends to $\alpha$ as $r\to0$ through positive real radii. This predicate alone does not assert finite energy, a positive denominator, or containment of coordinate balls.

OrderDefinedAt. The order is defined at $x$ when there exists $r_0>0$ such that, for every real $r$ satisfying $0<r<r_0$ , the closed coordinate ball of radius $r$ is contained in the coordinate domain, the KS energy on the corresponding open ball is strictly below infinity, and the real conversion of the boundary moment is strictly positive. The final positivity excludes both zero and infinite extended boundary moments, since toReal sends infinity to zero. This predicate does not itself assert convergence of the frequency quotient.

IsRankOne. IsRankOne N means exactly $N=1$ .

PossibleOrdersProblem. Given $N$ , Coxeter data $C$ , a complete metric Borel space $X$ , a Hausdorff second-countable complex one-manifold $S$ , Euclidean-building data $B$ of type EuclideanBuildingData N C X, a connected open domain $D\subseteq S$ , a map $u:S\to X$ , and a point $x_0\in D$ , this proposition says: if $u$ is KS-harmonic on $D$ and is nonconstant there, then the order is defined at $x_0$ ; there exist natural numbers $m,k$ with $m>0$ , $k>0$ , $k\le m$ , and $k$ dividing the finite cardinality of $C$ ’s orthogonal subgroup, such that the surface frequency tends to the real number $m/k$ at $x_0$ ; and, if $N=1$ , there exists a possibly unrelated natural number $m\ge2$ such that the same frequency tends to $m/2$ at $x_0$ . The building argument $B$ is not used anywhere in the defining formula after making the proposition well-typed. If harmonicity fails, or if harmonicity holds but nonconstancy fails, the proposition is true vacuously. The rank-one existential uses a new $m$ and states no explicit relation to the earlier pair $(m,k)$ .

Human review

Endorsed by Shuze Chen · Aug 27, 2026
Endorsed by ShouqiaoWang · Aug 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph