The Maximal Spectral Sharpness Theorem

Abstract

Spectral sharpness is the attained distance-normalized capacity, with its median-cut witness, qubit formula, endpoints, and data-processing law.

Theorem 1.1 (Spectral sharpness is the attained normalized capacity).

$$\begin{array}{c}\forall n\in \mathbb{N},r:\mathrm{Fin}(n+2)\to \mathbb{R},\\ (\forall i,0\le r_i)\wedge \mathrm{Antitone}(r)\wedge \sum _i{r}_i=1\Rightarrow \\ (\forall a:\mathrm{Fin}(n+2)\to \mathbb{R},\mathrm{Antitone}(a)\Rightarrow \mathrm{IsLeast}(\left\{d\mid \exists c\in \mathbb{R},\forall i,|a_i-c|\le d\right\},D(a)))\wedge \\ \mathrm{IsGreatest}(\left\{v\mid \exists a:\mathrm{Fin}(n+2)\to \mathbb{R},\mathrm{Antitone}(a)\wedge 0<D(a)\wedge \frac{C_a(r)}{D(a)}=v\right\},\mathrm{Sharp}(r))\wedge \\ ((\forall i,Q_n(i)=1\vee Q_n(i)=-1)\wedge \mathrm{Antitone}(Q_n)\wedge D(Q_n)=1\wedge \frac{C_{Q_n}(r)}{D(Q_n)}=\mathrm{Sharp}(r))\wedge \\ (\forall q:\mathrm{Fin}(2)\to \mathbb{R},\sum _i{q}_i=1\Rightarrow \mathrm{Sharp}(q)=\sqrt{2\sum _i{q}_i^2-1})\wedge \\ (\mathrm{Sharp}(r)=1⟺|\left\{i\mid r_i\ne 0\right\}|\le \frac{n+2}{2})\wedge \\ (\mathrm{Sharp}(r)=0⟺\forall i,r_i=\frac{1}{n+2})\wedge \\ (\forall r^{\prime }:\mathrm{Fin}(n+2)\to \mathbb{R},S:\mathrm{Matrix}(\mathrm{Fin}(n+2),\mathrm{Fin}(n+2),\mathbb{R}),\mathrm{Antitone}(r^{\prime })\wedge \mathrm{DS}(S)\wedge r=S{r}^{\prime }\Rightarrow \mathrm{Sharp}(r)\le \mathrm{Sharp}(r^{\prime })).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Sharpness/MaximalSpectralSharpness.maximal_spectral_sharpness (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let r be a nonnegative, nonincreasing, unit-sum spectrum in dimension N = n + 2. Its spectral sharpness Sharp(r) is one half the l1 distance from r to its reversal. For a nonincreasing observable spectrum a, D(a) is half its endpoint range. The first clause identifies D(a) as the least uniform bound on distance from a constant spectrum, so it is exactly the operator-norm distance from the observable to the center.

Sharp(r) is the greatest attained value of C_a(r)/D(a) over noncentral nonincreasing observables. The explicit median-cut question Q_n has only plus-or-minus-one values, is nonincreasing, has D(Q_n) = 1, and attains the greatest value. Thus the variational maximum and the yes/no maximizer are both addressable parts of the public statement.

For a two-point unit-sum spectrum q, Sharp(q) equals the square root of twice its quadratic purity minus one, the spectral form of the qubit Bloch radius. The same statement gives Sharp(r) = 1 exactly when the nonzero support has size at most N/2, and Sharp(r) = 0 exactly when r is uniform.

Finally, if r = S r’ for a doubly stochastic matrix S and both spectra are nonincreasing, then Sharp(r) <= Sharp(r’). This is the spectral majorization form of the unital-channel data-processing law. The proof uses the same median question on both sides and applies the frozen spectral-pairing comparison, rather than introducing a second channel or majorization carrier.

Dimension at least two is encoded by N = n + 2 because the normalized ratio ranges over observables outside the center. The numerical trials and decimal certificate accompanying the source statement are empirical checks and are not theorem clauses.

References

• Truth anchor: D5/S3/Quantum/Sharpness/MaximalSpectralSharpness.maximal_spectral_sharpness
• Dependency: D5/S3/Quantum/Sharpness/SpectralSharpnessDuality
• Dependency: D5/S3/Quantum/Sharpness/SpectralSharpnessSaturation