The Constructive Cost of Quantum Entanglement: Tsirelson Bound and Bell State Entropy in Lean 4

Paper 11 in the Constructive Reverse Mathematics of Mathematical Physics series. We provide a complete Lean 4 formalization of two foundational results in quantum information theory: Part A — Tsirelson bound: For any self-adjoint involutions A, A', B, B' on ℂ² and unit vector ψ ∈ ℂ² ⊗ ℂ², the CHSH operator satisfies ‖Cψ‖² ≤ 8, equivalently |⟨ψ, Cψ⟩| ≤ 2√2. Part B — Bell state entropy: The partial trace of the Bell singlet density matrix yields the maximally mixed state ρ_A = (1/2)I with von Neumann entropy S(ρ_A) = log 2. The formalization comprises 639 lines of Lean 4 across 8 modules, compiles with zero sorry, zero errors, and zero warnings. All theorems carry the axiom profile [propext, Classical.choice, Quot.sound] — standard Mathlib infrastructure axioms only. No custom axioms are introduced. Within the constructive reverse mathematics (CRM) programme, these results calibrate the compositional layer of quantum mechanics — tensor products, entanglement, correlations — establishing that Bell nonlocality and entanglement entropy are constructively accessible at the BISH level. This extends the calibration table from companion papers (Papers 2, 7, 8, 9) to cover relational quantum structure. Key finding: All logical costs arise from infinite-dimensional idealization, not from quantum compositional structure. Entanglement is constructively free. Archive contents: Lean 4 source code, LaTeX source, compiled PDF (20 pages), build instructions. Build: lake exe cache get && lake build — requires elan and ~8 GB disk space.