Step 4 · The corpus

Fifteen algorithms, and what was proved

Not toy circuits. Fourier transforms, block encodings, a qubitized walk, linear systems, topological data analysis, braiding, separability — each extracted from a Lean proof, each carrying the theorem that makes the extraction sound, and each with a deliberately broken variant the gate has to reject.

Fifteen exist rather than one because the hard part was done once. A construction is stated at the level it is natural — an operator, a chain complex, a braid word — and then lowered through mapped, proved transitions until it is an exact gate word over ℤ[ζ]. Each transition is a theorem, so the descent is mechanical rather than a fresh act of invention every time. That is the difference between designing one circuit and being able to design a family of them.

Circuit generation is slow enough that the field builds machinery to attack it directly: Quantinuum, NVIDIA and Pfizer’s ADAPT-GQE reports roughly an order of magnitude off circuit-generation time versus ADAPT-VQE. That work accelerates the search for a circuit. This one removes the search where a construction already exists — and hands you a proof either way.

Twelve of fifteen are axiom-free. Three are not, and say so: both Fourier rows depend on propext and Quot.sound, and the disjoint-support row also on Classical.choice. By this project’s own rule those are kernel-checked but not strictly constructive — so they are printed, not rounded up.