Local Spectral Floors

Abstract

Parity sectors and the local positive cone determine the full spectral floor.

Theorem 1.1 (Parity decomposition of the spectral infimum).

$$\forall Even\in Type,Odd\in Type,evenEnergy\in Even\to \mathrm{Real}\left(\right),evenNormSq\in Even\to \mathrm{Real}\left(\right),oddEnergy\in Odd\to \mathrm{Real}\left(\right),oddNormSq\in Odd\to \mathrm{Real}\left(\right),\left(\mathrm{Zero}\left(Even\right)\wedge \left(\mathrm{Zero}\left(Odd\right)\wedge \left(\mathrm{Nontrivial}\left(Even\right)\wedge \left(\mathrm{Nontrivial}\left(Odd\right)\wedge \left(\mathrm{apply}\left(evenEnergy,0\right)=0\wedge \left(\mathrm{apply}\left(oddEnergy,0\right)=0\wedge \left(\mathrm{apply}\left(evenNormSq,0\right)=0\wedge \left(\mathrm{apply}\left(oddNormSq,0\right)=0\wedge \left(\left(\forall e\in Even,\left(\neg e=0\right)\Rightarrow 0<\mathrm{apply}\left(evenNormSq,e\right)\right)\wedge \left(\left(\forall o\in Odd,\left(\neg o=0\right)\Rightarrow 0<\mathrm{apply}\left(oddNormSq,o\right)\right)\wedge \left(\mathrm{BddBelow}\left(\left\{\exists e\in Even,\left(\neg e=0\right)\wedge r=\mathrm{div}\left(\mathrm{apply}\left(evenEnergy,e\right),\mathrm{apply}\left(evenNormSq,e\right)\right)\mid r\in \mathrm{Real}\left(\right)\right\}\right)\wedge \mathrm{BddBelow}\left(\left\{\exists o\in Odd,\left(\neg o=0\right)\wedge r=\mathrm{div}\left(\mathrm{apply}\left(oddEnergy,o\right),\mathrm{apply}\left(oddNormSq,o\right)\right)\mid r\in \mathrm{Real}\left(\right)\right\}\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \mathrm{let}fullValues=\left\{\exists e\in Even,o\in Odd,\left(\neg \mathrm{pair}\left(e,o\right)=\mathrm{pair}\left(0,0\right)\right)\wedge r=\mathrm{div}\left(\mathrm{add}\left(\mathrm{apply}\left(evenEnergy,e\right),\mathrm{apply}\left(oddEnergy,o\right)\right),\mathrm{add}\left(\mathrm{apply}\left(evenNormSq,e\right),\mathrm{apply}\left(oddNormSq,o\right)\right)\right)\mid r\in \mathrm{Real}\left(\right)\right\},\mathrm{let}evenValues=\left\{\exists e\in Even,\left(\neg e=0\right)\wedge r=\mathrm{div}\left(\mathrm{apply}\left(evenEnergy,e\right),\mathrm{apply}\left(evenNormSq,e\right)\right)\mid r\in \mathrm{Real}\left(\right)\right\},\mathrm{let}oddValues=\left\{\exists o\in Odd,\left(\neg o=0\right)\wedge r=\mathrm{div}\left(\mathrm{apply}\left(oddEnergy,o\right),\mathrm{apply}\left(oddNormSq,o\right)\right)\mid r\in \mathrm{Real}\left(\right)\right\},\mathrm{sInf}\left(fullValues\right)=\min \left(\mathrm{sInf}\left(evenValues\right),\mathrm{sInf}\left(oddValues\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaAnalytic/LocalSpectralFloor.parity_spectral_infimum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The full carrier is the even-odd product. Additivity of energy and squared norm makes every mixed Rayleigh quotient a positive weighted average of the two sector quotients, while pure-sector vectors attain both comparison infima.

Theorem 1.2 (White-noise cone margin).

$$\forall H\in Type,quadratic\in H\to \mathrm{Real}\left(\right),normSq\in H\to \mathrm{Real}\left(\right),\left(\mathrm{Zero}\left(H\right)\wedge \left(\mathrm{Nontrivial}\left(H\right)\wedge \left(\mathrm{apply}\left(quadratic,0\right)=0\wedge \left(\mathrm{apply}\left(normSq,0\right)=0\wedge \left(\left(\forall f\in H,\left(\neg f=0\right)\Rightarrow 0<\mathrm{apply}\left(normSq,f\right)\right)\wedge \mathrm{BddBelow}\left(\left\{\exists f\in H,\left(\neg f=0\right)\wedge r=\mathrm{div}\left(\mathrm{apply}\left(quadratic,f\right),\mathrm{apply}\left(normSq,f\right)\right)\mid r\in \mathrm{Real}\left(\right)\right\}\right)\right)\right)\right)\right)\right)\Rightarrow \mathrm{let}rayleighValues=\left\{\exists f\in H,\left(\neg f=0\right)\wedge r=\mathrm{div}\left(\mathrm{apply}\left(quadratic,f\right),\mathrm{apply}\left(normSq,f\right)\right)\mid r\in \mathrm{Real}\left(\right)\right\},\mathrm{let}admissibleFloors=\left\{\forall f\in H,0\le \mathrm{sub}\left(\mathrm{apply}\left(quadratic,f\right),\mathrm{mul}\left(lambda,\mathrm{apply}\left(normSq,f\right)\right)\right)\mid lambda\in \mathrm{Real}\left(\right)\right\},\mathrm{sInf}\left(rayleighValues\right)=\mathrm{sSup}\left(admissibleFloors\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaAnalytic/LocalSpectralFloor.white_noise_cone_margin (✓ std3). ∎

Source. Repository-derived.

Commentary.

An admissible white-noise floor is exactly a lower bound of the nonzero Rayleigh-value set. The supremum of all such lower bounds is therefore the spectral infimum.

References

• Truth anchor: D5/S3/Weil/ZetaAnalytic/LocalSpectralFloor.parity_spectral_infimum
• Truth anchor: D5/S3/Weil/ZetaAnalytic/LocalSpectralFloor.white_noise_cone_margin