Agency Reserve Stability
Abstract
A positive singular-value reserve is the sharp perturbation radius preserving an agency dimension.
Theorem 1.1 (Reserve controls robust rank and its sharp boundary).
Proof. Machine-checked in Lean as D5/S3/Observer/AgencyReserveStability.agency_reserve_stability (✓ std3). ∎
Source. Repository-derived.
Commentary.
The index k is zero-based and represents the source’s one-based agency dimension r = k + 1. This avoids truncated natural subtraction in the rank-at-most-(r-1) comparison class.
Eckart-Young-Mirsky and continuity of the selected singular value are explicit premises because pinned Mathlib supplies neither theorem. The low-rank set is nevertheless constructively nonempty, containing the zero operator.
Any smaller perturbation cannot enter the low-rank set, by the defining lower bound for infimum distance. An attaining best approximation constructs a perturbation exactly at the reserve whose selected singular value is zero, proving boundary sharpness.
Continuity places a neighborhood of the base point inside every safe region with threshold below the reserve. Mathlib’s singular-value support theorem then keeps at least k + 1 range dimensions throughout a local neighborhood.
References
- Truth anchor:
D5/S3/Observer/AgencyReserveStability.agency_reserve_stability