The circle of a homogeneous harmonic map is locally an ellipse in an apartment of the atlas
DisprovedHarmonicBuilding.circleApartmentRepresentationInApartmentLet be a conical Euclidean building of type and rank , with apartment atlas , and let be a nonconstant homogeneous harmonic map of order about the origin. Then there is a such that around every base angle the image of the unit circle lies in a single apartment of the building, on which it is an ellipse centred at the cone point: there are a chart , a point of the model apartment with , and vectors such that
Role. This is the sharpened form of the local flatness of the circle. It differs from HarmonicBuilding.circleApartmentRepresentation in one respect only: the flat containing the arc is a member of the building's atlas, not merely an isometric copy of the model apartment. That distinction is invisible to every statement that reads one arc at a time — the chord law, the constant-distance rigidity, the orthonormality of the frame — but it is exactly what is needed to compare the charts of two overlapping arcs, since the compatibility axiom for apartments applies to atlas members and to nothing else. Without it the frames of different arcs live in unrelated copies of and the passage from local flatness to a closed billiards path cannot begin.
The mathematical content is unchanged: homogeneity and the regularity theorem for harmonic maps into buildings confine the singular set of to the origin, so each point of the circle has a neighbourhood whose image lies in one apartment ; writing in coordinates on with the cone point at , the harmonic map equation in polar coordinates reduces to , whose solutions are . The apartment supplied by the regularity argument is an apartment of the building, so it belongs to the atlas.
Formalization note. The base point is carried explicitly rather than normalized to the origin of the model apartment. An atlas is closed under precomposition with the affine Weyl group only, which in general contains no translation taking to , so demanding would be a strictly stronger requirement than the geometry provides. Forgetting the atlas membership and translating by recovers HarmonicBuilding.circleApartmentRepresentation.
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.
import Definitions.Def_frame_2026_harmonic_building_conical
namespace HarmonicBuilding
universe v
theorem circleApartmentRepresentationInApartment
{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 v1 v2 : ModelEuclideanSpace N,
c p0 = h 0 ∧
∀ theta : ℝ, |theta - theta0| < delta →
h (circlePoint 0 1 theta)
= c (p0 + (Real.cos (alpha * theta) • v1
+ Real.sin (alpha * theta) • v2)) := by sorry
end HarmonicBuilding