The Free-Negentropy Budget

Abstract

Density-state sharpness is controlled by negentropy, with monotone forgetting and sharp endpoint laws.

Definition 1.1 (The ordered density-state spectrum).

$$\forall n\in Type,rho\in \mathrm{DensityState}\left(n\right),\left(\mathrm{Fintype}\left(n\right)\wedge \mathrm{DecidableEq}\left(n\right)\right)\Rightarrow \mathrm{stateSpectrum}\left(\rho \right)=\left(eigenvalue{s}_0\right)\left(\mathrm{densityMatrix}\left(\rho \right)\right)$$

Formalization. D5/S3/Quantum/Sharpness/FreeNegentropyBudget.stateSpectrum (✓ std3).

Source. Repository-derived.

Commentary.

The spectrum is constructed from the canonical density matrix by taking the decreasing real eigenvalue family of its positive-semidefinite Hermitian representative. It is not defined from any target bound.

Theorem 1.2 (Von Neumann entropy is Shannon entropy of the ordered spectrum).

$$\forall n\in Type,rho\in \mathrm{DensityState}\left(n\right),\left(\mathrm{Fintype}\left(n\right)\wedge \mathrm{DecidableEq}\left(n\right)\right)\Rightarrow \mathrm{vonNeumannEntropy}\left(\rho \right)=\mathrm{shannonEntropy}\left(\mathrm{stateSpectrum}\left(\rho \right)\right)$$

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

Source. Repository-derived.

Commentary.

Finite-dimensional spectral calculus expands the trace-log definition over the density matrix eigenvalues. Reindexing those eigenvalues in decreasing order gives the stated Shannon entropy identity.

Theorem 1.3 (Sharpness, forgetting, and endpoint budgets).

$$\begin{gathered} \forall n\in Type,rho\in \mathrm{DensityState}\left(n\right),\left(\mathrm{Fintype}\left(n\right)\wedge \left(\mathrm{DecidableEq}\left(n\right)\wedge \mathrm{Nonempty}\left(n\right)\right)\right)\Rightarrow \mathrm{let}r:\mathrm{Fin}\left(\mathrm{card}\left(n\right)\right)\to \mathbb{R}:=\mathrm{stateSpectrum}\left(\rho \right); \\ \mathrm{let}u:\mathrm{Fin}\left(\mathrm{card}\left(n\right)\right)\to \mathbb{R}:=(i:\mathrm{Fin}\left(\mathrm{card}\left(n\right)\right)\mapsto \frac{1}{\mathrm{card}\left(n\right)}); \\ \mathrm{let}q:\mathbb{R}\to \left(\mathrm{Fin}\left(2\right)\to \mathbb{R}\right):=(x:\mathbb{R}\mapsto (i:\mathrm{Fin}\left(2\right)\mapsto \mathrm{ite}\left(i=0,\frac{1}{2}+\frac{x}{2},\frac{1}{2}-\frac{x}{2}\right))); \\ \begin{array}{c}\left(\forall i\in \mathrm{Fin}\left(\mathrm{card}\left(n\right)\right),0\le r\left(i\right)\right)\wedge \sum _{i\in \mathrm{Fin}\left(\mathrm{card}\left(n\right)\right)}r\left(i\right)=1\wedge \\ \mathrm{Antitone}\left(r\right)\wedge \\ \mathrm{vonNeumannEntropy}\left(\rho \right)=\mathrm{shannonEntropy}\left(r\right)\wedge \\ \mathrm{IsGreatest}\left(\{v:\mathbb{R}\mid \exists a\in \mathrm{Fin}\left(\mathrm{card}\left(n\right)\right)\to \mathbb{R},\left(\forall i\in \mathrm{Fin}\left(\mathrm{card}\left(n\right)\right),\left|a\left(i\right)\right|\le 1\right)\wedge \mathrm{spectralPairingCapacity}\left(r,a\right)=v\},\mathrm{spectralSharpness}\left(r\right)\right)\wedge \\ \mathrm{spectralSharpness}\left(r\right)\le 2\cdot \mathrm{totalVariation}\left(r,u\right)\wedge 2\cdot \mathrm{totalVariation}\left(r,u\right)\le \mathrm{sqrt}\left(2\cdot \left(\log \left(\mathrm{card}\left(n\right)\right)-\mathrm{vonNeumannEntropy}\left(\rho \right)\right)\right)\wedge \\ \mathrm{spectralSharpness}{\left(r\right)}^2\le 2\cdot \left(\log \left(\mathrm{card}\left(n\right)\right)-\mathrm{vonNeumannEntropy}\left(\rho \right)\right)\wedge \\ \forall sigma\in \mathrm{DensityState}\left(n\right),S\in \mathrm{Matrix}\left(\mathrm{Fin}\left(\mathrm{card}\left(n\right)\right),\mathrm{Fin}\left(\mathrm{card}\left(n\right)\right),\mathbb{R}\right),\left(\mathrm{doublyStochastic}\left(S\right)\wedge r=\mathrm{mulVec}\left(S,\mathrm{stateSpectrum}\left(sigma\right)\right)\right)\Rightarrow \begin{array}{c}\mathrm{spectralSharpness}\left(r\right)\le \mathrm{spectralSharpness}\left(\mathrm{stateSpectrum}\left(sigma\right)\right)\wedge \\ \mathrm{shannonEntropy}\left(\mathrm{stateSpectrum}\left(sigma\right)\right)\le \mathrm{shannonEntropy}\left(r\right)\wedge \\ \log \left(\mathrm{card}\left(n\right)\right)-\mathrm{shannonEntropy}\left(r\right)\le \log \left(\mathrm{card}\left(n\right)\right)-\mathrm{shannonEntropy}\left(\mathrm{stateSpectrum}\left(sigma\right)\right)\wedge \\ \forall a\in \mathrm{Fin}\left(\mathrm{card}\left(n\right)\right)\to \mathbb{R},\mathrm{Antitone}\left(a\right)\Rightarrow \mathrm{spectralPairingCapacity}\left(r,a\right)\le \mathrm{spectralPairingCapacity}\left(\mathrm{stateSpectrum}\left(sigma\right),a\right).\end{array}\wedge \\ \forall x\in \mathbb{R},\left(0\le x\wedge x\le 1\right)\Rightarrow \begin{array}{c}\left(\forall i\in \mathrm{Fin}\left(2\right),0\le q\left(x\right)\left(i\right)\right)\wedge \sum _{i\in \mathrm{Fin}\left(2\right)}q\left(x\right)\left(i\right)=1\wedge \\ \mathrm{Antitone}\left(q\left(x\right)\right)\wedge \\ \mathrm{shannonEntropy}\left(q\left(x\right)\right)=\mathrm{shannonEntropy}\left(\mathrm{positiveBiasLaw}\left(\frac{x}{2}\right)\right)\wedge \\ \mathrm{spectralSharpness}\left(q\left(x\right)\right)=x\wedge \\ 2\cdot \mathrm{totalVariation}\left(\mathrm{positiveBiasLaw}\left(\frac{x}{2}\right),\mathrm{positiveBiasLaw}\left(0\right)\right)=x.\end{array}\wedge \\ \mathrm{Tendsto}\left((x:\mathbb{R}\mapsto \frac{2\cdot \mathrm{totalVariation}\left(\mathrm{positiveBiasLaw}\left(\frac{x}{2}\right),\mathrm{positiveBiasLaw}\left(0\right)\right)}{\mathrm{sqrt}\left(2\cdot \left(\log \left(2\right)-\mathrm{shannonEntropy}\left(\mathrm{positiveBiasLaw}\left(\frac{x}{2}\right)\right)\right)\right)}),\mathrm{nhdsWithin}\left(0,\mathrm{Ioi}\left(0\right)\right),\mathrm{nhds}\left(1\right)\right)\wedge \\ \mathrm{IsBigO}\left((x:\mathbb{R}\mapsto 2\cdot \left(\log \left(2\right)-\mathrm{shannonEntropy}\left(\mathrm{positiveBiasLaw}\left(\frac{x}{2}\right)\right)\right)-{\left(2\cdot \mathrm{totalVariation}\left(\mathrm{positiveBiasLaw}\left(\frac{x}{2}\right),\mathrm{positiveBiasLaw}\left(0\right)\right)\right)}^2-\frac{x^4}{6}),\mathrm{nhds}\left(0\right),(x:\mathbb{R}\mapsto x^6)\right)\wedge \\ \mathrm{spectralSharpness}\left(r\right)=1\Rightarrow \begin{array}{c}\mathrm{rank}\left(\mathrm{densityMatrix}\left(\rho \right)\right)\le \lfloor \frac{\mathrm{card}\left(n\right)}{2}\rfloor \wedge \\ \mathrm{vonNeumannEntropy}\left(\rho \right)\le \log \left(\mathrm{rank}\left(\mathrm{densityMatrix}\left(\rho \right)\right)\right)\wedge \\ \mathrm{vonNeumannEntropy}\left(\rho \right)\le \log \left(\lfloor \frac{\mathrm{card}\left(n\right)}{2}\rfloor \right).\end{array}.\end{array} \end{gathered}$$

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

Source. Repository-derived.

Commentary.

For a density state on a nonempty finite carrier, let r be its ordered spectrum and u the uniform spectrum. Spectral sharpness is the greatest bounded spectral pairing and is at most twice total variation from u, which Pinsker bounds by the square root of twice the von Neumann entropy deficit. Squaring gives the quantitative free-negentropy budget.

A supplied doubly stochastic spectral mixing witness models forgetting. It decreases sharpness and every antitone pairing capacity, increases Shannon entropy, and therefore decreases the entropy deficit.

The canonical symmetric two-point law realizes the qubit endpoint. Its sharpness and twice-total-variation are the radius, the Pinsker ratio tends to one at the mixed endpoint, and the fourth-order residual has coefficient one sixth with a sixth-order remainder. At sharpness one, the density-matrix rank is at most half the dimension and controls the remaining entropy.

The source’s random-spectrum trial count, floating-point alert review, and seven-digit numerical comparison are empirical certificate remarks outside the named theorem. The exact inequalities, limit, expansion, and rank endpoint are the formalized clauses.

References

• Truth anchor: D5/S3/Quantum/Sharpness/FreeNegentropyBudget.free_negentropy_budget
• Truth anchor: D5/S3/Quantum/Sharpness/FreeNegentropyBudget.stateSpectrum
• Truth anchor: D5/S3/Quantum/Sharpness/FreeNegentropyBudget.von_neumann_entropy_eq_shannon_state_spectrum
• Dependency: D5/S3/Quantum/Divergence/VonNeumannEntropyPinching
• Dependency: D5/S3/Quantum/Dynamics/ProjectionProbabilityFlow
• Dependency: D5/S3/Quantum/Sharpness/SpectralPairingCapacity
• Dependency: D5/S3/Quantum/Sharpness/SpectralSharpnessDuality
• Dependency: D5/S3/Quantum/Sharpness/SpectralSharpnessSaturation
• Dependency: D5/S3/TotalVariation/Asymptotics/SymmetricBernoulliSecondOrder
• Dependency: D5/S3/TotalVariation/SpectralSharpnessNegentropyBudget