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

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.