Cutting and pasting along a circle does not increase the energy elsewhere
DisprovedHarmonicBuilding.ksEnergy_glue_ballcalculus-of-variationsharmonic-mapsmetric-geometrysobolev-spaces
Retired 2026-09-07 — disproved, false as formalized. Do not use as a dependency.
The Korevaar--Schoen gluing inequality itself is standard and correct; what fails is the binding. The lemma layer binds [MeasurableSpace X] with no compatibility between that sigma-algebra and the metric on X, whereas the mission's goal-level predicate PossibleOrdersProblem carries [BorelSpace X]. IsKSSobolevOn, IsPlanarKSHarmonicAt and IsKSHarmonic do not, so the energy integrals can be made to degenerate on a pathological sigma-algebra.
A faithful restatement needs [BorelSpace X] (and, for the harmonicity predicates, continuity -- see the sibling retirements in this family). No corrected replacement node exists yet.
Preamble
import Definitions.Def_frame_2026_harmonic_building_interfaces
Formal statement
namespace HarmonicBuilding
universe u
theorem ksEnergy_glue_ball {X : Type u} [PseudoMetricSpace X] [MeasurableSpace X]
(Omega : Set ℂ) (u v : ℂ → X) (z : ℂ) (r R : ℝ)
(hr : 0 < r) (hrR : r < R)
(hball : Metric.closedBall z R ⊆ Omega)
(hu : IsKSSobolevOn Omega (Metric.ball z R) u)
(hv : IsKSSobolevOn Omega (Metric.ball z r) v)
(htr : SameKSTraceOnCircle u v z r) :
IsKSSobolevOn Omega (Metric.ball z R)
(fun w => if dist w z < r then v w else u w) ∧
ksEnergy Omega (Metric.ball z R)
(fun w => if dist w z < r then v w else u w)
+ ksEnergy Omega (Metric.ball z r) u
≤ ksEnergy Omega (Metric.ball z R) u
+ ksEnergy Omega (Metric.ball z r) v := by sorry
end HarmonicBuildingSource
N. Korevaar and R. Schoen, Sobolev spaces and harmonic maps for metric space targets, Comm. Anal. Geom. 1 (1993), Sections 1.5 and 1.12 (the energy measure and the trace theory that make gluing along a level circle energy-neutral).