About This Visualization Suite
These interactive pages document the formal machine-checked proof of Wilde Quantum Information Theory in Lean 4.33.1 and Mathlib v4.33.0. The visualization platform merges two state-of-the-art interactive formalization visual paradigms:
-
Anthropic's Fermat's Last Theorem Architecture: Direct client-side execution of Graphviz compiled to WebAssembly (
@hpcc-js/wasm) embedded inassets/vendor/graphviz.umd.js, allowing users to dynamically expand and collapse dependency graphs on-the-fly without a server. - The Axiomatic-DRE Radial Dependency Tree Framework: Concentric multi-tier radial tree mapping high-level mathematical goals to atomized, independently solvable sub-problems, with real-time decentralized agent proof status tracking and verification rollup.
Soundness & Kernel Axioms
Every proof in the transitive closure of theorem13_4_2_atDilation has been replayed and verified through the Lean 4 kernel with 0 sorrys. The logical foundations rest strictly upon Lean's three standard classical axioms:
| Kernel Axiom | Type | Role in Quantum Proofs |
|---|---|---|
Classical.choice |
{α : Sort u} → Nonempty α → α |
Non-constructive existence of orthonormal bases, spectral projections, and operator limits. |
propext |
{a b : Prop} → (a ↔ b) → a = b |
Propositional extensionality; allows replacement of logically equivalent statements in proofs. |
Quot.sound |
{α : Sort u} {r : α → α → Prop} → r a b → Quot.mk r a = Quot.mk r b |
Soundness of quotient types; fundamental for the algebraic construction of tensor products $S \otimes T$. |
Offline & Standalone Design
This entire documentation package is 100% self-contained:
- Graphviz Layout: Bundled WebAssembly binary (`graphviz.umd.js`, 802 KB).
- KaTeX Mathematics Typesetting: Offline bundled engine (`katex.min.js`, 265 KB) with base64-embedded fonts (`katex-embedded.css`).
- Zero Network Latency: Can be served from any static file server or inspected directly over
file://URLs.
Textbook Reference
Mark M. Wilde, Quantum Information Theory (2nd Edition, Cambridge University Press, 2017).