The mass-triangle inequality and its recorded consequences #
This file owns the public conclusions of the subadditivity chain. It removes
the phase-one hypothesis by head--tail octahedral induction, inhabits the named
targets stated in HeartShortExact, and derives the unconditional topology
comparison from the conditional substrate in Metric.Distance.Topology.
This is the module a consumer of the milestone should import.
Mass is subadditive for a distinguished triangle whose first object lies
in the phase-one slice. The proof first cuts the middle object at phase zero;
the common lower tail splits off exactly from both the middle and right
objects. It then cuts the remaining right object at phase two; the common
upper head again splits off exactly. The residual triangle lies in the
two-cohomology window (0, 2], where
stabilityMass_triangle_le_of_obj₁_phase_one_of_amplitude applies.
The second mass-triangle milestone: the triangle inequality whenever the left endpoint is semistable, at an arbitrary phase. A lifted rotation moves that phase to one and preserves every object's HN mass.
Harder--Narasimhan mass is subadditive along every distinguished triangle.
Full-distance balls form a neighbourhood basis for the pre-existing Section 6 topology. This closes the explicit mass-triangle premise of the topology comparison without installing a second topology or metric instance.
The global distinguished-triangle inequality restricts to the heart-level short-exact inequality.
A short exact sequence in the heart of the slicing satisfies the mass inequality when its middle object is semistable in the ambient slicing.
A short exact sequence in the heart satisfies the mass inequality when its endpoint objects are semistable of the same phase.