Autoequivalences preserve the full stability distance #
The phase coordinates were handled in WeakStabilityCondition/StabilityCondition/Metric/Isometry/Phase.lean. The new input is
AutPair.act_stabilityMass: transporting every HN filtration through the
equivalence preserves its finite charge-norm sum, so it preserves the HN
mass. The three coordinates can then be transported
objectwise, and the two supremum inequalities use Φ⁻¹ E and Φ E exactly as
in the phase-only proof.
The final quotient theorem is the full-distance analogue of
AutPairQuot_smul_slicingDist. It is still stated for AutPairQuot v, not
for the paper's bare Aut(D). The trust annotation records that remaining
group-level boundary rather than identifying this theorem with Lemma 8.2.
The acted φ⁺ discrepancy at E is the original discrepancy at Φ⁻¹E.
The acted φ⁻ discrepancy at E is the original discrepancy at Φ⁻¹E.
The acted logarithmic mass discrepancy at E is the original discrepancy
at Φ⁻¹E.
All three objectwise coordinates transport through the inverse-image object.
Forward-object form of the objectwise three-coordinate invariance.
A compatible autoequivalence pair preserves the complete three-coordinate stability distance.
The compatible autoequivalence group acts by full-distance isometries.