The semi-closed and closed upper half-planes #
Two subsets of ℂ and the three facts about them that every consumer needs.
Nothing here is categorical, algebraic or stability-theoretic: the statements
quantify over complex numbers and use Complex.arg alone.
Placement #
These declarations were introduced beside their first consumer, the central
charge conditions in StabilityCondition/Weak/Charge.lean, and that file's own
docstring recorded them as an upstream candidate for
Mathlib/Analysis/Complex/UpperHalfPlane/. MO1.13 (#1324) acted on that: the
Euclidean core of the mass-subadditivity proof must be importable without
categories and without stability, and it cannot be while a half-plane
membership predicate lives inside the stability tree. The nearest owner at the
pinned Mathlib revision is Analysis/Complex/, so that is the path.
The namespace is deliberately not changed. CategoryTheory reads oddly over
an analysis file and the oddity is accepted rather than repaired: a namespace
cutover would rename declarations and invalidate the immutable review payloads
that exe/RestateHistoricalNames.lean exists to protect. This is standing
decision 1 of the cutover ledger.
The closed upper half-plane: the weak condition, which unlike
semiClosedUpperHalfPlane contains 0. That single difference is the whole of
the weak/strict distinction, and it is why μ-slope stability on a surface is weak
— a skyscraper has zero rank and zero degree, so its μ-charge is 0.