A quantum circuit, verified
The circuit that prepares the Bell state, step by step — each step anchored to a Lean theorem from the ZX corpus. Exact morphism equality, not numeric simulation.
Starting point: two qubits in the state |00⟩. In FinHilb the state is a morphism 𝟙 ⟶ Q⊗Q — preparing a state is already an arrow in the category.
State: |00⟩