Maximum Spectral-Floor Completion

Abstract

Residual positivity and full-spectrum white-floor feasibility have the same maximum.

Theorem 1.1 (Maximum spectral-floor completion).

$$\forall Spectrum\in \mathrm{Type}\left(\right),Reading\in \mathrm{Type}\left(\right),check\in \mathrm{AddMonoidHom}\left(Spectrum,Reading\right),white\in \mathrm{NNReal}\left(\right)\to Spectrum,delta\in Reading,source\in Reading,\left(\forall floor\in \mathrm{NNReal}\left(\right),check\left(white\left(floor\right)\right)=\mathrm{toReal}\left(floor\right)\cdot delta\right)\Rightarrow \left(\left(\forall floor\in \mathrm{NNReal}\left(\right),\mathrm{ResidualFeasible}\left(check,delta,source,floor\right)\iff \mathrm{FullSpectrumFeasible}\left(check,white,source,floor\right)\right)\wedge \mathrm{sSup}\left(\{floor\mid \mathrm{ResidualFeasible}\left(check,delta,source,floor\right)\}\right)=\mathrm{sSup}\left(\{floor\mid \mathrm{FullSpectrumFeasible}\left(check,white,source,floor\right)\}\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/MaximumSpectralFloorCompletion.maximum_spectral_floor_completion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The positive spectrum carrier packages nonnegativity. A floor is locally feasible when removing its normalized white reading leaves the reading of a positive residual spectrum.

From a local residual, adding the white spectrum constructs an explicit full-spectrum witness. Conversely, a full-spectrum decomposition returns its residual as the local witness.

Thus the two feasible-floor predicates agree pointwise. Their defining sets are equal, so their conditionally complete suprema are equal, including the empty or unbounded cases supplied by NNReal.

References

• Truth anchor: D5/S3/Weil/MaximumSpectralFloorCompletion.maximum_spectral_floor_completion