Axiomatic Lineage & Foundational Trace
Tracing every theorem, lemma, and exercise across all 28 chapters of Mark M. Wilde's Quantum Information Theory back to the physical postulates of quantum mechanics and the formal logical kernel of Lean 4.
The Axiomatic Hierarchy of Quantum Information Theory
In formal mathematics and mathematical physics, a proof is only as sound as its foundational assumptions. Axiomatic-DRE provides transparent, auditable lineage tracing for every statement:
● Tier 0: Lean 4 Kernel Axioms
The logical bedrock of dependent type theory. Only 3 primitive axioms are admitted:
Classical.choice: Non-constructive existence of spectral projectors and orthonormal bases.propext: Propositional Extensionality ((P ↔ Q) ⇒ P = Q).Quot.sound: Quotient Soundness for Hilbert tensor products and equivalence classes.
● Tier 1: Mathlib Functional Analysis
Rigorous operator algebra and continuous real analysis:
- Spectral Theorem: Diagonalization of compact self-adjoint operators into real eigenvalues.
- Trace Cyclicity: Basis-independence of trace and partial trace contractivity.
- Logarithm Calculus at Zero: Continuity of x \log x ensuring 0 \log 0 = 0.
- Jensen's Inequality: Finite convex combination inequalities.
● Tier 2: Physical Quantum Postulates
The physical principles of quantum mechanics (Nielsen & Chuang / Wilde, Ch. 3–4):
- Postulate 1 (State Space): Density operators \rho \ge 0, \operatorname{Tr}(\rho) = 1.
- Postulate 2 (Observables): POVMs \{M_m\} and Born rule p(m) = \operatorname{Tr}(M_m \rho).
- Postulate 3 & 6 (Composite Systems): Tensor products \mathcal{H}_A \otimes \mathcal{H}_B and partial trace \operatorname{Tr}_B.
- Postulate 5 (Evolution): Unitary dynamics U^\dagger U = \mathbb{I} and CPTP quantum channels.
Interactive Axiomatic Lineage Matrix
Select any landmark theorem, lemma, or exercise to inspect its physical postulates, upstream mathematical lemmas, and logical axioms. Click Trace in Graphviz → to render the complete DAG in WebAssembly.
| Declaration | Chapter & Role | Quantum Postulates | Mathlib Bedrock | Kernel Axioms | Action |
|---|---|---|---|---|---|
| Loading declarations matrix… | |||||