Quantum and Circuits
Quantum models, channel interfaces, and circuit constructions.
Completion: Reading edition complete · Lean: Selected results recorded · Confidence: Recorded formal evidence
Before you start
Suggested background: Complex vectors and matrices, orthogonal projectors, and finite Fourier transforms for the arithmetic and symmetry parts; linear algebra and explicit gate costs for the catalytic part; Boolean functions and polynomials over the binary field for the circuit part. The introductory measurement example below offers a shorter starting point.
Recorded results and limits: Complete 344-page publication with explicit open research. 211 named declarations across thirteen formal modules cover selected arithmetic/circuit developments, not the full book.
Remaining work: Map the remaining ordinary-proof chapters and open physical targets separately from the thirteen checked modules.
The background advice is an editorial starting point. The work itself states its prerequisites and hypotheses.
Reading routes · Glossary · Claim links · Download this work
Start here: choose a visual introduction, full study, or formal companion. Each path links directly to the HTML edition and explains useful background.
A route through the volume
The book asks what a change of representation makes accessible, and what it costs to reach, update, and reconstruct that representation. Its four treatments use distinct models.
| Treatment | Chapters | Question to follow |
|---|---|---|
| Arithmetic realizations | 1–2 | How does an arithmetic selector become a Fourier projector and a normalized quantum state? Begin with the twelve-dimensional example. |
| Symmetry collapse | 3–7 | When do invariant packets and moving frames give an accessible simulation? Track coordinate, update, and measurement costs alongside dimension. |
| Catalytic gate set distortion | 8–12 | Can temporarily leaving a restricted gate model reduce cost while restoring the required boundary state? Keep the gate alphabet and resource convention fixed. |
| Circuit obstructions | 13–21 | What do restoration, safe discrepancy covers, and projection imply within the stated circuit and linear-summary models? |
Start with chapters 1–2, then choose the treatment closest to your question. Appendices A–F give the formal and computational companions, claim coverage, and verification boundaries. The glossary and collected references follow them.
Read with the evidence
The recorded formal inventory has 96 arithmetic declarations and 115 circuit declarations across thirteen modules. These include supporting statements. They cover selected developments; the symmetry and catalytic treatments retain their written arguments and bounded computational evidence.
For circuits, the formal companion covers C01, the sharing-aware degree dependency, and the numerical C02 bound. Read the maintained claim register for C03–C08 and their written or finite evidence. Universal efficient quantum simulation, unrestricted circuit hardness, and the wider catalytic synthesis questions remain open in this edition.
Formal replay requirements and exact coverage · Current circuit claim register
Try the arithmetic phase example
Follow the modulus-12 calculation, then change the phase in the browser. Compare coherent sign replacement with coordinate dephasing. The exact Python program reproduces this finite teaching example using the standard library; it does not run Lean.
Worked examples for this work
These introductory calculations lead into this work’s subject. The source and evidence links below retain the work’s recorded scope.
Complete demonstration with runnable code: Quantum phase, measurement, and information loss.
Read
- Read online: complete volume, appendices, proofs and sources
- Edition README
- Read PDF
- Visual guide (PDF)
Back to work navigation · Worked examples
Written proofs
Read the written arguments in the PDF. The manuscript source remains available below.
Find the statement number or section in the reading files, then read its assumptions and argument. A claim map may cover only part of the written result.
- Manuscript text (TeX)
- Current circuit claim register (C01–C08)
- Historical circuit claim register (preserved companion)
Find this work among other written proofs
Back to work navigation · Worked examples
Lean
Start with the edition guide and the build instructions below. Check the correspondence records to see which written claims the Lean declarations cover. Source links lead to .lean files. PDF guides explain the formalization.
- Formal replay: setup, pinned runtime, and coverage
- Lean guide (PDF)
- Quantum Lean source snapshot
- Circuit Lean source snapshot
- Current circuit claim register (C01–C08)
- Historical circuit claim register (preserved companion)
Find this work among other Lean projects
Back to work navigation · Worked examples
Code
These links include code, examples, checks, or build tools. Read the edition guide for setup instructions and what each command does. All software is beta and work in progress.
- Portable formal replay wrapper (requires the external Lean kit)
- Symmetry packet implementation and exact checks
- Catalytic gate atlas: mathematical modules
- Circuit scientific replay (Python and C++17)
Find this work among other code projects
Back to work navigation · Worked examples
Evidence
- Completion, Lean coverage, confidence, and cited evidence
- Source-file receipt (identity and availability)
- All files in this source edition
The evidence records describe the reviews and runs completed for this edition.
Back to work navigation · Worked examples