What question did this study set out to answer?

The aim is to formalize the non-reflexivity of trace-class operators and its relation to the Weak Limited Principle of Omniscience.

February 11, 20260 citationsOpen Access

The Physical Bidual Gap and Banach Space Non-Reflexivity: A Lean 4 Formalization of WLPO via Trace-Class Operators

PLPaul Lee

Key Points

The aim is to formalize the non-reflexivity of trace-class operators and its relation to the Weak Limited Principle of Omniscience.
Formalization established using Lean 4 with 754 lines of code across 8 files.
Proof relies on applications of the Hahn-Banach theorem, excluding James's theorem.
Comparison made with a companion formalization for ℓ¹ non-reflexivity.
Demonstrated that the trace-class operators are not reflexive as a Banach space.
Established that every closed subspace of reflexive Banach space remains reflexive.
Identified the bidual gap containing singular states not expressible as density matrices.

Abstract

We present a Lean 4 formalization establishing that the trace-class operators S₁ (H) on a separable Hilbert space are not reflexive as a Banach space, and that any constructive witness of this non-reflexivity implies the Weak Limited Principle of Omniscience (WLPO). In the algebraic formulation of quantum mechanics, S₁ (H) is the canonical state space of density matrices; the bidual gap (S₁ (H) ) ** \ J (S₁ (H) ) contains singular states not representable by any density matrix. The formalization comprises 754 lines of Lean 4 code across 8 files (Mathlib4 v4. 28. 0-rc1), with one interface assumption bridging a companion formalization for ℓ¹ non-reflexivity. The key technical contribution is a machine-checked proof that every closed subspace of a reflexive Banach space is reflexive, using two applications of the Hahn-Banach theorem without James's theorem. Extends Paper 2 (doi: 10. 5281/zenodo. 18501689) from the abstract c₀/ℓ¹ setting to the physically motivated trace-class operator setting. Version 1. 1 change: P7Minimal addition, revised paper Other papers in the Constructive Reverse Mathematics Series (see Zenodo for current files): Paper 1: WithdrawnPaper 2: Bidual gap and WLPO — DOI: 10. 5281/zenodo. 17107493Paper 3: WithdrawnPaper 4: Quantum spectra axiom calibration — DOI: 10. 5281/zenodo. 17059483Paper 5: Schwarzschild curvature verification — DOI: 10. 5281/zenodo. 18489703Paper 6: Heisenberg uncertainty (v2, CRM over Mathlib) — DOI: 10. 5281/zenodo. 18519836Paper 7: Physical bidual gap, trace-class operators — DOI: 10. 5281/zenodo. 18527559Paper 8: 1D Ising model and LPO — DOI: 10. 5281/zenodo. 18516813Paper 9: Ising formulation-invariance — DOI: 10. 5281/zenodo. 18517570Paper 10: Logical geography of mathematical physics — DOI: 10. 5281/zenodo. 18527877Paper 11: Entanglement, CHSH, Tsirelson bound — DOI: 10. 5281/zenodo. 18527676Paper 12: Constructive history of mathematical physics — DOI: 10. 5281/zenodo. 18528793Paper 13: Event horizon as logical boundary — DOI: 10. 5281/zenodo. 18529007 Note: GitHub repository is not maintained; please see Zenodo for current files.

问 AI

Bookmark

View Full Paper