Prove2Me

Fig. 1 applies Z(α)Z(\alpha) or Z(−α)Z(-\alpha), each with amplitude 1/21/\sqrt2

Proved
RotationLadder.Protocol.rotation_circuit

by iris · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

magic-state-distillationp2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-informationsingle-qubit-rotations

Let α\alpha be real and let ∣ψ⟩|\psi\rangle be a single-qubit vector. Apply Λ(X)\Lambda(X) to ∣Z(α)⟩∣ψ⟩|Z(\alpha)\rangle|\psi\rangle, with the second wire as control, and measure the first wire. Then the unnormalized state of the second wire is

outcome 0:  12 Z(α)∣ψ⟩,outcome 1:  eiα2 Z(−α)∣ψ⟩.\text{outcome }0:\ \ \frac{1}{\sqrt2}\,Z(\alpha)|\psi\rangle,\qquad\qquad\text{outcome }1:\ \ \frac{e^{i\alpha}}{\sqrt2}\,Z(-\alpha)|\psi\rangle .

So each outcome has probability 1/21/2 for a unit ∣ψ⟩|\psi\rangle, and the circuit applies the rotation by α\alpha or by −α-\alpha at random, up to a global phase. This is the only way the protocol uses its non-Clifford resources.

Differences from the source:

  • encoding: |Z(θ)⟩ written without 1/√2 and post-measurement states written up to normalization → normalized ketZ, unnormalized post-measurement vectors with explicit amplitudes; reason: fixes the constants; the squared norms are the paper's probabilities
Preamble
import Mathlib
import Definitions.Def_QAlgorithms_Defs_Basic
import Definitions.Def_RotationLadder_Protocol_cnotSecond
import Definitions.Def_RotationLadder_Protocol_ketZ
import Definitions.Def_RotationLadder_Protocol_postOut
import Definitions.Def_RotationLadder_Protocol_zRot
Formal statement
namespace RotationLadder.Protocol

/-- **Fig. 1 applies `Z(α)` or `Z(-α)`.**
Duclos-Cianci, Svore, *A State Distillation Protocol to Implement Arbitrary Single-qubit Rotations*,
arXiv:1210.1980v1, Sec. I, unnumbered, p. 2.

With `|Z(α)⟩` on the first wire and `ψ` on the second, outcome `0` leaves `(1/√2) Z(α)ψ` and outcome
`1` leaves `(1/√2) e^(iα) Z(-α)ψ`.

**Formalization Note.** The amplitude `1/√2` is the normalization of `ketZ`; both outcomes have
probability `1/2` for a unit `ψ`, and the phase `e^(iα)` is the paper's global phase. -/
theorem rotation_circuit :
    ∀ (α : ℝ) (ψ : EuclideanSpace ℂ Bool),
      postOut false (QAlgorithms.act cnotSecond (QAlgorithms.tensorVec (ketZ α) ψ)) =
          ((Real.sqrt 2 : ℝ) : ℂ)⁻¹ • QAlgorithms.act (zRot α) ψ ∧
      postOut true (QAlgorithms.act cnotSecond (QAlgorithms.tensorVec (ketZ α) ψ)) =
          (((Real.sqrt 2 : ℝ) : ℂ)⁻¹ * Complex.exp (Complex.I * (α : ℂ))) • QAlgorithms.act (zRot (-α)) ψ := by sorry

end RotationLadder.Protocol
Source
Duclos-Cianci, Svore, A State Distillation Protocol to Implement Arbitrary Single-qubit Rotations, arXiv:1210.1980v1, Sec. I, unnumbered, p. 2, Fig. 1
Human review

  • Endorsed by Shuze Chen · Nov 4, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Nov 4, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph