The mathematics under Four Quantum Oracles: five chapters, each derived by hand and checked by a script with controls that must fail.
| Chapter | What it derives and checks |
|---|---|
| QM1 · States, gates, tensor products | Unit vectors, unitary gates, the Pauli algebra, entanglement, no-cloning |
| QM2 · Measurement and CHSH | Born rule, Schmidt decomposition, CHSH reaching 2√2 and no further |
| QM3 · Fourier transform and phase estimation | The QFT as matrix and circuit; phase estimation; continued fractions |
| QM4 · Order finding and Shor | The reduction, the exact distribution, Shor's bounds, the lemma checked to 400 |
| QM5 · Braiding: Fibonacci and Ising | Braid relation, finite Ising closure, non-closing Fibonacci, a typo in the source |
Every chapter has a qmN-verify.py beside it, standard library only; where the chapter leans on a source PDF the script extracts it from ~/Downloads and prints SKIP, never PASS, if it is not there.
The Lean file Orthogenesis/Quantum/QubitAlgebra.lean states the Pauli algebra, a Clifford conjugation and the abstract no-cloning argument; it has not been compiled and is not yet imported from Orthogenesis.lean.
Scope. This is the mathematics, checked at toy sizes on a classical machine. It makes no claim about quantum hardware, error correction at scale, or any application; and it does not treat Shor's discrete-logarithm algorithm, Grover's proof of optimality, the Solovay–Kitaev theorem, or the stabiliser formalism.