Exact Sticky Reduction

Abstract

Completing a positive complementary block preserves positivity and negative inertia.

Theorem 1.1 (Exact sticky reduction).

$$\forall HP\in \mathrm{Type}\left(\right),HQ\in \mathrm{Type}\left(\right),APP\in \mathrm{LinearMap}\left(\mathbb{R},HP,HP\right),AQP\in \mathrm{LinearMap}\left(\mathbb{R},HP,HQ\right),AQQ\in \mathrm{LinearMap}\left(\mathbb{R},HQ,HQ\right),AQQInv\in \mathrm{LinearMap}\left(\mathbb{R},HQ,HQ\right),\left(\mathrm{NormedAddCommGroup}\left(HP\right)\wedge \left(\mathrm{InnerProductSpace}\left(\mathbb{R},HP\right)\wedge \left(\mathrm{NormedAddCommGroup}\left(HQ\right)\wedge \left(\mathrm{InnerProductSpace}\left(\mathbb{R},HQ\right)\wedge \left(\left(\forall q\in HQ,0\le \mathrm{inner}\left(\mathrm{apply}\left(AQQ,q\right),q\right)\right)\wedge \left(\left(\forall x\in HQ,y\in HQ,\mathrm{inner}\left(\mathrm{apply}\left(AQQ,x\right),y\right)=\mathrm{inner}\left(x,\mathrm{apply}\left(AQQ,y\right)\right)\right)\wedge \mathrm{comp}\left(AQQ,AQQInv\right)=\mathrm{id}\left(\mathbb{R},HQ\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\left(\left(\forall z\in \mathrm{Prod}\left(HP,HQ\right),0\le \mathrm{apply}\left(\mathrm{blockEnergy}\left(APP,AQP,AQQ\right),z\right)\right)\iff \left(\forall p\in HP,0\le \mathrm{apply}\left(\mathrm{schurEnergy}\left(APP,AQP,AQQ,AQQInv\right),p\right)\right)\right)\wedge \mathrm{negativeIndex}\left(\mathrm{blockEnergy}\left(APP,AQP,AQQ\right)\right)=\mathrm{negativeIndex}\left(\mathrm{schurEnergy}\left(APP,AQP,AQQ,AQQInv\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaLinear/ExactStickyReduction.exact_sticky_reduction (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let HP and HQ be real inner-product spaces representing the retained and complementary summands. The full block energy and its Schur energy are constructed from APP, AQP, AQQ, and a right inverse of AQQ.

Assume the complementary block is nonnegative and symmetric. Then the full energy is nonnegative exactly when the Schur energy is, and their negative inertia indices agree.

The negative index is the supremum of dimensions of finite negative-definite subspaces, so the statement remains meaningful when HQ is infinite-dimensional. The proof completes the square and transports every finite negative subspace in both directions.

References

• Truth anchor: D5/S3/Weil/ZetaLinear/ExactStickyReduction.exact_sticky_reduction