Interior Lipschitz regularity of a planar Korevaar--Schoen minimizer at the centre
DisprovedHarmonicBuilding.lipschitzAtCenter_of_isPlanarKSHarmonicOnRetired 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 lipschitzAtCenter_of_isPlanarKSHarmonicOn
{N : ℕ} {C : EuclideanCoxeterData N}
(M : ConicalBuildingModel.{v} N C) (h : ℂ → M.carrier)
(hharm : IsPlanarKSHarmonicOn Set.univ h) :
∃ K r : ℝ, 0 < r ∧
∀ z : ℂ, ‖z‖ < r → dist (h z) (h 0) ≤ K * ‖z‖ := by sorry
end HarmonicBuilding