Book-Scale Formalization Metrics
The 6 Parts of the Treatise
Part I: Concepts & Classical Shannon Theory (Ch. 1–2)
Classical entropy, asymptotic equipartition property (AEP), Shannon source coding theorem, channel capacity, and Fano's inequality.
Part II: The Postulates of Quantum Mechanics (Ch. 3–5)
State space, density matrices, composite systems, observables, completely positive trace-preserving (CPTP) maps, Kraus operators, and Uhlmann's theorem.
Part III: Protocols & Distance Measures (Ch. 6–9)
Teleportation, super-dense coding, coherent protocols, unit resource capacity region, trace distance contractivity, and fidelity.
Part IV: Quantum Entropies & Information (Ch. 10–13)
von Neumann entropy, Strong Subadditivity (Lieb-Ruskai), Lieb concavity theorem, quantum data processing, and Theorem 13.4.2 (Mutual Info Concavity).
Part V: Typicality & Data Compression (Ch. 14–18)
Classical and quantum typicality, the non-commutative operator packing lemma, quantum covering lemma, and Schumacher compression.
Part VI: Channel Capacities & Coding Theorems (Ch. 19–28)
The grand capacity theorems: Holevo-Schumacher-Westmoreland (HSW), BSST entanglement-assisted capacity, private capacity, and the Lloyd-Shor-Devetak (LSD) theorem.
Axiomatic Foundations & Quantum Postulate Tracing
● 4 Physical Quantum Postulates
State space (\( ho \ge 0, \operatorname{Tr} ho=1\)), observables (POVM Born rule), composite systems (\mathcal{H}_A \otimes \mathcal{H}_B), and unitary/CPTP channel evolution.
● Mathlib Operator Bedrock
The continuous Spectral Theorem for Hermitian operators, cyclic trace invariance, Jensen's inequality, and logarithm calculus at zero (0 \log 0 = 0).
● 3 Lean 4 Kernel Axioms
Classical.choice, propext, and Quot.sound. No unproved hypotheses, zero circularity, and verified 0 sorrys.
Landmark Capacity Theorem: LSD Quantum Capacity (Theorem 24.3)
Lloyd-Shor-Devetak (LSD) Quantum Capacity:
The quantum channel capacity $Q(\mathcal{N})$ for transmitting uncorrupted qubits without error equals the regularized coherent information $I(A \rangle B) = H(B) - H(E)$ of the channel.