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.
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.
In 1964, John Bell showed that any local hidden‑variable theory must satisfy a specific inequality on correlations between distant measurements. In its CHSH form (Clauser, Horne, Shimony, Holt 1969), the inequality reads |S| = |E(a,b) + E(a,b′) + E(a′,b) − E(a′,b′)| ≤ 2, where E(a,b) is the correlation between measurement outcomes at two separated parties using settings a and b. Any local realist theory respects this bound. Quantum mechanics violates it. Experiments confirm the violation. The standard quantum prediction for a maximally entangled state with optimal measurement angles is |S| = 2√2 ≈ 2.828. In 1980, Boris Tsirelson proved that 2√2 is not just one quantum prediction — it is the *maximum* value any quantum correlation can produce. No quantum state, no measurement scheme, no clever protocol can push |S| beyond 2√2. The bound is sharp, the value is exact, and it has been measured in laboratories around the world to experimental precision. The Tsirelson bound is one of the deepest empirical structures in physics. It tells us that quantum correlations exceed classical correlations by a specific, finite amount — there is room to violate Bell’s inequality, but only so much room. The number 2√2 has no obvious physical interpretation. It does not appear in the formulation of quantum mechanics. It emerges from the mathematics of the bipartite Hilbert space when the CHSH operator is constructed and bounded. The question is where it comes from. In standard QM, the answer is that it falls out of the Hilbert‑space structure plus Cauchy–Schwarz plus an operator‑norm bound on the CHSH operator. Technically correct, and Tsirelson’s 1980 proof remains the canonical derivation — but it leaves the deeper structure unanswered. The Hilbert space is postulated. The inner product that makes Cauchy–Schwarz available is postulated. The bipartite tensor‑product structure on H_A ⊗ H_B is postulated. The 2√2 value is what those postulates produce when run through the CHSH operator. This walkthrough shows how the Event Density framework derives the Tsirelson bound from a smaller set of structural commitments. The Hilbert‑space structure, the inner product, and the bipartite tensor‑product structure all emerge as forced consequences of the substrate ontology rather than being postulated. With those structures forced rather than assumed, Tsirelson’s 1980 argument applies directly, and the 2√2 value is no longer the output of a chain of postulates but the output of a chain of derived theorems. Like Heisenberg, Bell–Tsirelson is a place where the framework’s contribution is upstream. The bound itself is mathematical physics already in the literature; what changes is the foundational status of the structures the argument requires. ED does not produce a new derivation step beyond standard QM here — it removes the postulational status of the structures the standard derivation already uses. The 2√2 value is now a derived consequence of the substrate ontology, all the way down.
Quantum information theory is built on entropic quantities; among them, the sandwiched Rényi relative entropy is a fundamental divergence with various applications, and its data processing inequality (DPI) under quantum channels is a cornerstone result. In this work, we present a Lean 4 library for quantum information, designed as a reusable formal infrastructure for theoretical analysis. As a central demonstration of the library, we formalize the DPI for the sandwiched Rényi relative entropy for positive semidefinite operators on finite-dimensional quantum systems. The library provides a basis-independent operator-theoretic framework for finite-dimensional quantum mechanics compatible with the standard mathematical library Mathlib, including reusable interfaces for finite-dimensional systems, states, channels, tensor products, partial traces, Choi operators, Kraus representations, and Stinespring representations. It also builds infrastructure for noncommutative trace inequalities, including operator monotonicity and convexity via the real continuous functional calculus, block-operator positivity, Hilbert-Schmidt operator spaces, Jensen's operator inequality, generalized perspectives, operator power means, and Lieb-Ando trace inequalities. On top of this framework, we formalize entropy-specific ingredients for the DPI: variational formulas for the sandwiched quasi-entropy via Young and reverse-Young inequalities, tensor-product compatibility of real powers, and Haar measures on unitary groups. Together, these components yield a Lean formalization of the DPI, give strong subadditivity as a corollary, and provide the last missing component needed to complete the Lean formalization of the generalized quantum Stein's lemma. More broadly, the development provides machine-checkable foundations for future formalized and AI-assisted research in quantum information theory.
Synthesis and interpretive companion to the Constructive Calibration Programme (Papers 2-16). Contains no new theorems. Assembles machine-verified results from six companion papers into a single calibration table mapping layers of quantum theory to positions in the constructive hierarchy of omniscience and choice principles. The calibration table establishes: finite-volume physics and preparation uncertainty (Heisenberg inequality) are fully constructive (BISH); measurement uncertainty and locale spatiality require Dependent Choice (DC_omega); exact spectral membership requires Markov's Principle (MP, orthogonal axis); the bidual gap and singular states require WLPO; the thermodynamic limit requires LPO; and the spectral gap is undecidable. The logical geography forms a partial order, not a linear chain, with the omniscience spine (BISH < WLPO < LPO) as the dominant chain and DC_omega and MP as orthogonal dimensions. Proposes a working hypothesis: empirical predictions of quantum theory are BISH-derivable, and stronger principles enter only through idealizations no finite laboratory can instantiate. Reports a formulation-invariance test (Papers 8 and 9) showing the LPO cost of the thermodynamic limit is identical across transfer-matrix and combinatorial derivations. Includes comparisons with van Wierst, Batterman, Pour-El and Richards, Gisin, and the Doering-Isham topos program. Six open problems are posed. Includes a TikZ diagram of the logical geography. All formal results are verified in Lean 4 (predominantly CRM over Mathlib; Paper 4 uses AxCal). The Lean 4 formalizations and manuscripts were developed with substantial AI assistance. version1.1: This is the synthesis and conceptual companion to the author's constructive calibration programme (Papers 1–13). It contains no new theorems or Lean formalizations. Its purpose is to assemble the calibration table mapping layers of mathematical physics to positions in the constructive hierarchy (BISH < WLPO < LPO < LEM, with orthogonal axes DC_ω and MP), establish the series-wide certification methodology, formulate a working hypothesis, and pose open problems. What's New in v1.1: Certification methodology section (§3): New ~2-page section establishing three certification levels — mechanically certified (P2_Minimal, P7_Minimal), structurally verified (Papers 7-Full, 8A, 9A, 11, 13-BISH), and intentional classical content (Papers 8B, 13-LPO) — with discussion of the Mathlib question, the role of minimal artifacts, and limitations. This is the section referenced by Papers 7, 8, 11, and 13 for the series-wide methodology. Expanded calibration table: Five new rows from Paper 11 (Bell nonlocality, entanglement entropy, partial trace — all BISH) and Paper 13 (Schwarzschild interior finite-time physics — BISH; geodesic incompleteness — LPO). Table now contains 17 entries across four domains of mathematical physics. Strengthened working hypothesis: Evidence now spans functional analysis, statistical mechanics, quantum information, and general relativity. Domain invariance discussion: Papers 8 and 13 use BMC ≡ LPO in unrelated physical domains (thermodynamic limit vs. geodesic incompleteness), providing evidence that LPO costs are intrinsic to the physics. Two new open problems: Infinite-dimensional entanglement entropy (Problem 7) and singularity calibration beyond Schwarzschild/Penrose theorem (Problem 8). Fixed TikZ diagram: MP no longer incorrectly shown as implying WLPO (they are independent over BISH). Paper (23 pages, LaTeX source + compiled PDF). No Lean code — this is a conceptual/synthesis paper. License: CC-BY 4.0 - v 2.0 Add coverage of paper 13-16 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 — 10.5281/zenodo.18580342 [v 2.0 Technical Synthesis of paper 1-16]Paper 11: Entanglement, CHSH, Tsirelson bound — DOI: 10.5281/zenodo.18527676Paper 12: Constructive history of mathematical physics — DOI: 10.5281/zenodo.18528793 [v 2.0 historical synthesis of paper 1-16]Paper 13: Event horizon as logical boundary — DOI: 10.5281/zenodo.18529007 Paper 14: Quantum Decoherence - DOI: 10.5281/zenodo.18569068 Paper 15: Noether Theorem - DOI: 10.5281/zenodo.18572494 Paper 16: Technical Note Born Rule - DOI: 10.5281/zenodo.18575377 Note: GitHub repository is not maintained; please see Zenodo for current files.
Quantum information theory (QIT) characterizes the capabilities and fundamental limits of quantum information processing, underpinning quantum communication, computation, and error correction. Formalizing its coding theorems requires connecting finite-block protocols, analytic inequalities, and asymptotic limits within a unified machine-checked framework. Existing developments, however, lack a reusable operational layer that defines codes, error criteria, achievable rates, and capacities independently of their information-theoretic characterizations. In this work, we present LeanQIT, a Lean 4 library for finite-dimensional QIT. It provides composable, kernel-checked interfaces for quantum states and channels, source and channel codes, finite-block performance criteria, hypothesis testing, one-shot quantities, and asymptotic rate constructions. Using this infrastructure, we formalize Schumacher's quantum source-coding theorem, the Holevo--Schumacher--Westmoreland classical-capacity theorem, and the entanglement-assisted classical-capacity theorem together with its strong converse. By separating operational definitions from analytic characterizations and exposing reusable achievability, converse, and asymptotic components, Lean-QIT provides a machine-readable foundation for formal QIT and a compositional knowledge substrate for emerging AI-assisted formalization, automated proof search, and agentic reasoning in quantum information and computation.
In 1935, Einstein, Podolsky, and Rosen published the paper that introduced what would become quantum mechanics’ most studied phenomenon. Two systems prepared together and then separated remain correlated — perfectly correlated, in some cases — across arbitrary distances. The correlations exceed anything classical physics permits, are tested today across hundreds of kilometers via satellite‑mediated photon pairs, and form the resource that quantum cryptography, teleportation, and computation rely on. The standard QM account is mathematically clean. Two systems with Hilbert spaces H_A and H_B are described on H_A ⊗ H_B; states that cannot be written as |ψ_A⟩ ⊗ |ψ_B⟩ are entangled. Bell–Tsirelson bounds CHSH at 2√2. Schmidt decomposes any pure bipartite state biorthogonally. Coffman–Kundu–Wootters codifies monogamy. No‑signaling follows from linearity of partial trace. Von Neumann entropy S(ρ_A) = −Tr(ρ_A log ρ_A) measures entanglement strength. Each piece is a theorem of the postulated formalism — but the postulates themselves (tensor‑product joint structure, Hilbert space, Born rule) are not derived. This walkthrough shows how the Event Density framework derives the structural commitments themselves. Six results, each derived from the same substrate primitives: (1) Tensor‑product composition — the joint participation measure of two endpoints sharing one rule is carried on H_A ⊗ H_B with bilinearly induced inner product. Form forced; no auxiliary assumption. (2) Generic non‑factorizability — entangled states are dense and full‑measure; product states are the measure‑zero exception. (3) Schmidt decomposition — every pure bipartite state has a biorthogonal decomposition with non‑negative coefficients summing to one. Form forced; values inherited. (4) Monogamy — each substrate endpoint has a finite local cross‑chain bandwidth budget; full bipartite entanglement saturates it; no capacity remains for a third endpoint. CKW is the substrate bandwidth‑conservation law in concurrence units. (5) No‑signaling — over‑determined by three independent substrate locks: T18 forward‑cone‑only kernel structure, P11 commitment irreversibility, and the ED‑I‑06 no‑fundamental‑fields guardrail. (6) Von Neumann entropy — the form is uniquely picked by Shannon–Khinchin axioms each independently derived from named substrate primitives. This walkthrough has more substrate content than Bell–Tsirelson or Heisenberg. Those ran on standard mathematical‑physics arguments once the framework supplied the Hilbert space; the contribution was upstream. Here the framework is upstream for tensor‑product composition, Schmidt, and the density of entangled states — and substantively new for monogamy, no‑signaling, and entropy, each receiving a substrate‑mechanism account standard QM does not provide. The structural payoff: bipartite entanglement is what the substrate produces when two endpoints share one undeveloped participation rule. Tensor product, Schmidt structure, monogamy, no‑signaling, and entropy form are six projections of one substrate phenomenon.
This preprint proves a sharp purity bound for arbitrary complex pure states in tensor products of antisymmetric pair spaces, across the physical cut consisting of the first system from each pair versus the second system from each pair. For every finite number m of pairs and local dimensions at least two, purity is at most 2^(-m) and entanglement entropy is at least m bits, with equality characterized by products of normalized decomposable two-forms. It derives entanglement of formation m for m copies of the normalized antisymmetric state and, using the published regularization theorem, entanglement cost one ebit for every local dimension at least two. The archive provides original formal sources and a precise account of their scope; it does not claim a complete Lean translation of every ordinary LOCC execution. Research directed and curated by Matthew Liston. The mathematics, proofs, formalization and manuscript preparation substantially involve AI systems; paper-specific attribution and checking limits are disclosed in the paper and archive. No independent human proof verification, external endorsement or peer review is claimed. Licensing: original manuscript and documentation CC BY 4.0; original code MIT. The inherited QICLean SchattenNorm helper retains Apache 2.0 and its original attribution. The archive provides the exact file-level license mapping. Manuscript revision: 22 October 2026. Research director's note — Matthew Liston: This project is motivated by philosophical exploration and curiosity about AI-assisted research. My aim in sharing these results is to make them available for scrutiny, correction and further development, so that others can build on whatever proves useful to mathematics and science. Correspondence: atemporalwalk@gmail.com.