Prove2Me

34≤p0,i<cos⁡2π8\tfrac34\le p_{0,i}<\cos^2\frac{\pi}{8} and 0<θi<π40<\theta_i<\frac{\pi}{4}

Proved
RotationLadder.Protocol.ladder_bounds

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

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

For every level i≥0i\ge0,

34≤p0,i<cos⁡2π8=0.853…,0<θi<π4.\frac34\le p_{0,i}<\cos^2\frac{\pi}{8}=0.853\ldots,\qquad\qquad 0<\theta_i<\frac{\pi}{4}.

The walk on the ladder is therefore biased upward at every level, which is what makes each level cheap to reach.

Differences from the source:

  • reading: 0 < θ_i < π/4 (∀i) → every level i ≥ 0; reason: at i = −1, θ = π/4 and p = 1/2, so the paper's ∀i can only range over the levels of the ladder
  • encoding: cos²(π/8) = 0.853 . . . → 0.853 < cos²(π/8) < 0.854; reason: a truncated decimal says exactly this
Preamble
import Mathlib
import Definitions.Def_RotationLadder_Protocol_ladderProb
Formal statement
namespace RotationLadder.Protocol

/-- **The bounds on the ladder.**
Duclos-Cianci, Svore, *A State Distillation Protocol to Implement Arbitrary Single-qubit Rotations*,
arXiv:1210.1980v1, Sec. II, unnumbered, p. 3.

`3/4 ≤ p_(0,i) < cos²(π/8) = 0.853…` and `0 < θ_i < π/4` for every level `i ≥ 0`.

**Formalization Note.** Levels are natural numbers. At `i = -1`, `θ = π/4`, outside the printed
range; the paper's `∀i` ranges over the ladder's levels. -/
theorem ladder_bounds :
    (∀ i : ℕ, 3 / 4 ≤ ladderProb i ∧ ladderProb i < Real.cos (Real.pi / 8) ^ 2 ∧
      0 < theta i ∧ theta i < Real.pi / 4) ∧
    0.853 < Real.cos (Real.pi / 8) ^ 2 ∧ Real.cos (Real.pi / 8) ^ 2 < 0.854 := by sorry

end RotationLadder.Protocol
Source
Duclos-Cianci, Svore, A State Distillation Protocol to Implement Arbitrary Single-qubit Rotations, arXiv:1210.1980v1, Sec. II, unnumbered, p. 3
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