Certified Sticky Matrix

Abstract

A conservative finite lower form certifies Schur and full block positivity.

Theorem 1.1 (Finite lower matrix certification).

$$\forall HP\in Type,HQ\in Type,APP\in \mathrm{LinearMap}\left(\mathrm{Real}\left(\right),HP,HP\right),AQP\in \mathrm{LinearMap}\left(\mathrm{Real}\left(\right),HP,HQ\right),AQQ\in \mathrm{LinearMap}\left(\mathrm{Real}\left(\right),HQ,HQ\right),AQQInv\in \mathrm{LinearMap}\left(\mathrm{Real}\left(\right),HQ,HQ\right),delta\in \mathrm{Real}\left(\right),\left(\mathrm{NormedAddCommGroup}\left(HP\right)\wedge \left(\mathrm{InnerProductSpace}\left(\mathrm{Real}\left(\right),HP\right)\wedge \left(\mathrm{NormedAddCommGroup}\left(HQ\right)\wedge \left(\mathrm{InnerProductSpace}\left(\mathrm{Real}\left(\right),HQ\right)\wedge \left(0<delta\wedge \left(\left(\forall q\in HQ,\mathrm{mul}\left(delta,\mathrm{pow}\left(\mathrm{norm}\left(q\right),2\right)\right)\le \mathrm{inner}\left(\mathrm{Real}\left(\right),\mathrm{apply}\left(AQQ,q\right),q\right)\right)\wedge \left(\left(\forall x\in HQ,y\in HQ,\mathrm{inner}\left(\mathrm{Real}\left(\right),\mathrm{apply}\left(AQQ,x\right),y\right)=\mathrm{inner}\left(\mathrm{Real}\left(\right),x,\mathrm{apply}\left(AQQ,y\right)\right)\right)\wedge \mathrm{comp}\left(AQQ,AQQInv\right)=\mathrm{id}\left(\mathrm{Real}\left(\right),HQ\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\left(\left(\forall p\in HP,0\le \mathrm{sub}\left(\mathrm{inner}\left(\mathrm{Real}\left(\right),\mathrm{apply}\left(APP,p\right),p\right),\mathrm{mul}\left(\mathrm{inv}\left(delta\right),\mathrm{pow}\left(\mathrm{norm}\left(\mathrm{apply}\left(AQP,p\right)\right),2\right)\right)\right)\right)\Rightarrow \left(\forall p\in HP,0\le \mathrm{schurEnergy}\left(APP,AQP,AQQ,AQQInv,p\right)\right)\right)\wedge \left(\left(\forall p\in HP,0\le \mathrm{schurEnergy}\left(APP,AQP,AQQ,AQQInv,p\right)\right)\Rightarrow \left(\forall z\in \mathrm{Prod}\left(HP,HQ\right),0\le \mathrm{blockEnergy}\left(APP,AQP,AQQ,z\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaCore/CertifiedStickyMatrix.certified_sticky_matrix (✓ std3). ∎

Source. Repository-derived.

Commentary.

A positive complementary gap controls the coupling term. Positivity of the conservative lower form therefore implies Schur positivity, which implies positivity of the full block energy.

References

• Truth anchor: D5/S3/Weil/ZetaCore/CertifiedStickyMatrix.certified_sticky_matrix
• Dependency: D5/S3/Weil/ZetaLinear/ExactStickyReduction