Pole Capacity Rank One
Abstract
A positive rank-one pole update removes at most one negative direction.
Theorem 1.1 (A pole pair has negative-index capacity one).
Proof. Machine-checked in Lean as D5/S3/Weil/ZetaLinear/PoleCapacityRankOne.pole_capacity_rank_one (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let I be a finite carrier with decidable equality, let F0 be a Hermitian complex matrix on I, and let p be a complex vector. The updated matrix is constructed as F0 plus twice the canonical outer product of p with its conjugate.
The negative spectral index of the update is at least the original negative index minus one. If the updated matrix is positive semidefinite, the original negative index is therefore at most one.
The proof applies negative-index subadditivity to the updated matrix and the negative rank-one correction. Pinned Mathlib supplies the outer-product positivity and rank bound; repository searches found no theorem already stating both public clauses.
Theorem 1.2 (rank hermNegPart eq negIndex).
Proof. Machine-checked in Lean as D5/S3/Weil/ZetaLinear/PoleCapacityRankOne.rank_hermNegPart_eq_negIndex (✓ std3). ∎
Source. Repository-derived.
Commentary.
The negative spectral part has rank equal to the number of negative eigenvalues.
Theorem 1.3 (negDefOn range hermNegPart).
Proof. Machine-checked in Lean as D5/S3/Weil/ZetaLinear/PoleCapacityRankOne.negDefOn_range_hermNegPart (✓ std3). ∎
Source. Repository-derived.
Commentary.
The negative of a Hermitian matrix is positive definite on the range of its negative spectral part.