Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Full spectrum and faithful finite or Nat reference bases

Abstract

Complete spectral representation of the original positive trace-class operator.

Theorem 1.1 (Full nonnegative trace spectrum).

Proof. Machine-checked in Lean as D5/S3/Quantum/Analysis/TraceClass/Spectral.exists_nonneg_trace_spectral_data (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Mathlib contributors (2026). Compact self-adjoint spectral theorem and full Hilbert bases. URL: https://github.com/leanprover-community/mathlib4/blob/db584cd6d46c92f209a44c0f1c829460d327499d/Mathlib/Analysis/InnerProductSpace/Spectrum.lean.

Commentary.

H is an arbitrary complete complex Hilbert space, T is its actual bounded complex-linear operator, and trace is the analytic trace with its genuine IsTraceClass proof. The conclusion constructs w as a set of vectors in H, a full Hilbert basis b indexed by w, and real eigenvalues s. Every eigenspace is retained, including zero. The real eigenvalues are summable, have sum Re(trace T), and their complex casts have sum trace T. For each x, the weighted terms are (b.repr x i * (s i : Complex)) smul b i and have actual sum T(x). No basis, compactness, spectral carrier, separability or countability assumption is an input.

Theorem 1.2 (Faithful normalized reference).

Proof. Machine-checked in Lean as D5/S3/Quantum/Analysis/TraceClass/Spectral.exists_faithful_reference_spectral_data (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Mathlib contributors (2026). Compact self-adjoint spectral theorem and full Hilbert bases. URL: https://github.com/leanprover-community/mathlib4/blob/db584cd6d46c92f209a44c0f1c829460d327499d/Mathlib/Analysis/InnerProductSpace/Spectrum.lean.

Commentary.

The kernel is the actual linear-map kernel. Strictly positive weights follow because a zero eigenvalue would put a norm-one basis vector in that trivial kernel. Real summability and positivity then make the full index countable. Both the real and complex sums equal one, and the weighted expansion converges to the original sigma(x). Faithfulness gives no bounded inverse or uniform spectral gap.

Theorem 1.3 (Actual finite or Nat basis).

Proof. Machine-checked in Lean as D5/S3/Quantum/Analysis/TraceClass/Spectral.faithful_reference_finite_or_nat (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Mathlib contributors (2026). Compact self-adjoint spectral theorem and full Hilbert bases. URL: https://github.com/leanprover-community/mathlib4/blob/db584cd6d46c92f209a44c0f1c829460d327499d/Mathlib/Analysis/InnerProductSpace/Spectrum.lean.

Commentary.

The finite branch returns a natural number n, an actual Hilbert basis indexed by Fin n, positive weights, finite-dimensionality, both trace sums and the original-operator vector series. In the infinite branch a genuine equivalence from the source full index to Nat transports a full Hilbert basis and all scalar sums; the transported basis has the same weighted operator representation. A finite basis is never padded by zero vectors.

Construction: choose a Hilbert basis in each closed complex eigenspace. Mathlib’s orthogonal sigma-family theorem gives orthonormality. An ambient vector orthogonal to all these vectors is orthogonal to each full eigenspace by density; the compact symmetric spectral theorem makes it zero. HilbertBasis.mkOfOrthogonalEqBot therefore yields a full basis. Symmetry makes its eigenvalues real, and the nonnegative quadratic form makes them nonnegative. The accepted trace-class compactness theorem supplies compactness from the operator itself.

The analytic diagonal summability and positive trace-basis identity are the attributed Physlib suppliers in Library/QuantumBounds/diem2026traceclass.md. Rewriting the actual diagonal first establishes Summable s; only then is its real sum identified with the trace. Mapping b.hasSum_repr x through T proves the weighted series. This is a formal composition of standard spectral theory, not a new analytic spectral theorem or a solution of the entropy-continuity conjecture.

Boundary cases: zero on a nonseparable space retains its full zero eigenspace without a countability conclusion. A nonfaithful rank-one state does not satisfy the faithful adapter’s kernel premise. Positive summable eigenvalues may tend to zero. These endpoints do not assert logarithmic energy, entropy identities, heat-trace finiteness or an unbounded Hamiltonian.

References