The pasted map's energy is at most the sum over the two pieces

Let $u$ have finite Korevaar--Schoen energy on $B_R(z)$, let $v$ have finite energy on $B_r(z)$ with $0<r<R$, and suppose $u$ and $v$ have the same Sobolev trace on the circle $\partial B_r(z)$. Let $w$ be the cut-and-paste map, equal to $v$ inside $B_r(z)$ and to $u$ outside. Then $w$ has finite energy on $B_R(z)$, and

Role. This is the substantive half of the gluing lemma: the energy of the pasted map on the whole disc is no more than the sum of its energies on the two pieces. It fails without the trace hypothesis — a genuine jump across the circle contributes infinite energy — so this is exactly where matching traces is used. Combined with superadditivity of the energy, which is elementary, it gives the comparison

that lets a map minimizing energy at one radius be shown to minimize at every smaller radius.

Formalization note. The approximate energies are not subadditive over a set and its complement, because the density carried by the interface definition is truncated by the very set being integrated over, and that truncation grows with the set. Subadditivity is therefore a statement about the limit, and its proof goes through the Korevaar--Schoen energy measure together with the trace theory of that paper; the interface's finite-energy hypotheses on $u$ and $v$ are what make the two sides meaningful.

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.