The circle of a constant-distance homogeneous map lifts to a great circle
DisprovedHarmonicBuilding.circleLiftsToClosedBilliardsPathRetired 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 import Definitions.Def_spherical_great_circle
namespace HarmonicBuilding
universe v
theorem circleLiftsToClosedBilliardsPath
{N : ℕ} (C : EuclideanCoxeterData N) (M : ConicalBuildingModel.{v} N C)
(h : ℂ → M.carrier) (alpha L : ℝ)
(hhom : IsHomogeneousOfOrderOn M Set.univ h 0 alpha)
(hharm : IsPlanarKSHarmonicOn Set.univ h)
(hnc : NonconstantOn h Set.univ)
(hconst : ∀ theta : ℝ, dist (h (circlePoint 0 1 theta)) (h 0) = L) :
∃ (v1 v2 : ModelEuclideanSpace N) (w : C.weyl) (m : ℕ),
‖v1‖ = 1 ∧ ‖v2‖ = 1 ∧ inner ℝ v1 v2 = 0 ∧ 0 < m ∧
∀ s : ℝ, SphericalGeometry.greatCirclePath v1 v2 (s + 2 * Real.pi * alpha / m)
= (w : OrthogonalGroup N) (SphericalGeometry.greatCirclePath v1 v2 s) := by sorry
end HarmonicBuilding