### wai-quantum: rewrites, each checked, and equivalence proved by them at any width

Feature 11 of the co-design report: a verified-rewrite lens shared by the person and the assistant, and the general equivalence check it needs first.

- **The rewrites** (`engine::rewrite`): a gate and its inverse cancel; two rotations about one axis merge, and the phase gates add up (`t t` is `s`); a gate between two Hadamards becomes its conjugate (`h x h` is `z`, `h cx h` on the target is `cz`); a gate that does nothing is dropped; a gate is carried past gates it commutes with to cancel or merge with its partner; two gates that commute trade places. The rules propose and the engine decides: each rewrite's gates are checked against its replacement on just the qubits they touch, by tableau or on every basis state (`equiv::proved_equal`), so no rule is trusted.
- **Equivalence proved by rewriting** (`rewrite::prove`): one program followed by the other's inverse is rewritten toward nothing. When nothing is left, the two are the same unitary up to a global phase at any width and with any gates. `equiv::equivalent_programs` now tries it after the exact check and before random inputs, answering `how: rewrites`, which the workbench and the taste model count as a proof. When it does not reduce, nothing is concluded and the next check runs.
- **A chain** (`rewrite::explain`): both programs simplified to a fixed point and compared, gate for gate or, where they differ only in the order of gates that commute, by a proof. Each step is in words.
- **The lens** (`rewrite::options`): every rewrite a program admits as an edit to its own lines (a merge writes `rz(0.25 + 0.5)`, comments stay), read back and compared gate for gate before it is offered. A generator is rewritten as the circuit it writes out.
- **The command line:** `wai-quantum rewrite options | apply | simplify | explain`.
- **For agents:** `rewrite_qasm`.
- **The Studio:** "Rewrites" under the circuit (each rewrite in words, its gates marked on the diagram, "Take" to offer it as the engine's proposal, the list following the program); Alternatives says how the draft becomes a candidate that is the same circuit, as a chain; an equivalence proved by rewriting reads "by checked rewrites".
- **For hosts:** `rewrite::call`, `engine_rewrite` in the page, `rewrite` in the desktop app.
- **CI:** wai-web's native engine tests count 12.

