v0.2.0 — Stabilizer backend + verify_prob semantic automation

What's new

Verified stabilizer backend (Phase 2)

A fully-proved Aaronson-Gottesman tableau simulator for Clifford circuits.

• Stabilizer/StabTableau.lean -- 2n-row Boolean tableau; stepH/S/X/Z/CNOT; stabSim
• Stabilizer/Sound.lean -- stabSim_correct (core refinement theorem); zProb_correct; verify_stabilizer_prob_sound (unconditional, no hnorm)
• Stabilizer/CliffordGate.lean -- CliffordGate inductive; ofQCircuit? classifier + soundness
• Stabilizer/PauliGroup.lean -- Pauli group; Clifford conjugation lemmas

One known remaining sorry: zProbDet_eigenvalue (Z_q eigenstate claim for the deterministic measurement branch).

Benchmarks: GHZ(n) for n=1..200 all pass native_decide; n=200 in ~13s confirming O(n^2) scaling.

verify_prob tactic (Phase 1 + 2)

One tactic closes measurement-probability goals automatically:

-- Bell circuit
example : QCircuit.bellPrep |= .measurementProb QState.ket00 0 false (1/2) := by
  verify_prob

-- 100-qubit GHZ via stabilizer backend
example : (ghzCliffordCircuit 99).toQCircuit |=
    .measurementProb (ket0Vec 100, ket0Vec_norm 100) (0, by omega) false (1/2 : R) := by
  verify_prob

Clifford circuits dispatch to the stabilizer tableau backend (O(n^2)). Other circuits use the dense gate-by-gate evaluator.

Book chapter 8 updated

verify_prob one-liners for Bell/GHZ/Grover and a 100-qubit GHZ stabilizer proof. All 12 chapters build clean.

Documentation

• ARCHITECTURE.md: new 7.6 (verify_prob dispatch) and 7.7 (stabilizer backend design)
• README.md: theorem table split into structural/semantic; Stabilizer/ and Tactic/ added to layout
• FUTURE_WORK.md removed; replaced by SEMANTIC_ROADMAP.md

Using this release

require lean-qverify from git
  "https://github.com/akkeshavan/lean-qverify" @ "v0.2.0"

Previous release

v0.1.0.0 -- foundation, ZX-calculus, QHL, Python bridge, 40 kernel-checked theorems