LocallyPositiveSpectrum

Abstract

Finite-dimensional spectral and overlap bounds for antidistinguishability.

Theorem 1.1 (local psd negIndex).

$$\forall (n:\mathbb{N}),(1\le n)\to \forall (Y:Matrix(Finn)(Finn)\mathbb{C})(hY:LocallyPsdY),RHLinalg.negIndexhY.1\le 1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/LocallyPositiveSpectrum.local_psd_negIndex (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston, Vincent Russo, Jamie Sikora (2025). Tight bounds for antidistinguishability and circulant sets of pure quantum states. DOI: 10.22331/q-2025-02-04-1622. URL: https://arxiv.org/abs/2311.17047v2.

Commentary.

The formula states the complete estimate or implication. Matrix entries, finite index sets, and proof parameters retain their Lean meanings. Proof fields of finite-index constructors are omitted.

Theorem 1.2 (local psd kernel eq zero).

$$\forall (n:\mathbb{N})(Y:Matrix(Finn)(Finn)\mathbb{C}),(LocallyPsdY)\to \forall (v:Finn\to \mathbb{C}),(RHLinalg.hermFormYv<0)\to \forall (x:Finn\to \mathbb{C}),(Y{\times }_{v}x=0)\to x=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/LocallyPositiveSpectrum.local_psd_kernel_eq_zero (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston, Vincent Russo, Jamie Sikora (2025). Tight bounds for antidistinguishability and circulant sets of pure quantum states. DOI: 10.22331/q-2025-02-04-1622. URL: https://arxiv.org/abs/2311.17047v2.

Commentary.

The formula states the complete estimate or implication. Matrix entries, finite index sets, and proof parameters retain their Lean meanings. Proof fields of finite-index constructors are omitted.

Theorem 1.3 (local psd reciprocal budget).

$$\forall (n:\mathbb{N})(Y:Matrix(Fin(n+1))(Fin(n+1))\mathbb{C})(hY:LocallyPsdY)(p:Fin(n+1)),(hY.1.eigenvaluesp<0)\to (\forall (i:Fin(n+1)),i\ne p\to 0<hY.1.eigenvaluesi)\wedge (\sum i\in univ.erasep,(hY.1.eigenvaluesi{)}^{-1})\le (-hY.1.eigenvaluesp{)}^{-1}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/LocallyPositiveSpectrum.local_psd_reciprocal_budget (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston, Vincent Russo, Jamie Sikora (2025). Tight bounds for antidistinguishability and circulant sets of pure quantum states. DOI: 10.22331/q-2025-02-04-1622. URL: https://arxiv.org/abs/2311.17047v2.

Commentary.

The formula states the complete estimate or implication. Matrix entries, finite index sets, and proof parameters retain their Lean meanings. Proof fields of finite-index constructors are omitted.

References

• Truth anchor: D5/S3/Quantum/Measurement/LocallyPositiveSpectrum.local_psd_kernel_eq_zero
• Truth anchor: D5/S3/Quantum/Measurement/LocallyPositiveSpectrum.local_psd_negIndex
• Truth anchor: D5/S3/Quantum/Measurement/LocallyPositiveSpectrum.local_psd_reciprocal_budget
• Dependency: D5/S3/Quantum/Measurement/AntidistinguishabilityGram
• Dependency: D5/S3/Weil/ZetaLinear/PoleCapacityRankOne