Remark 7: unit-modulus ring scalars are eighth roots

Open

QAlgorithms.Papers.Independent.Intakethird100.P85.unitScalar_eighthRoot

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $z\in\mathbb Z[1/\sqrt2,i]$ and suppose $|z|=1$ . With $\omega=e^{i\pi/4}$ ,

\exists m\in\{0,1,\ldots,7\},\qquad z=\omega^m.

This is the scalar implication explaining the redundant final determinant condition in Corollary 2. It preserves absolute phase and also applies to zero-qubit unitary operators.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P85

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P85

open scoped Classical BigOperators

open QAlgorithms

open QAlgorithms.Papers.Independent.Gap48.P10
  (InZomega InDomega Residue bits residue residueMultiply Reducible)

open QAlgorithms.Papers.Independent.Support21.P13
  (synthesisRing integralRing coordinateValue HTLetter htWordMatrix EntriesInRing cliffordTLibrary)

local notation "omega" => QAlgorithms.gateT true true

local notation "sqrtTwo" => ((Real.sqrt 2 : ℝ) : ℂ)

/-- Remark 7, PDF p.6: unit-modulus ring scalars are exactly eighth-root powers. -/
theorem unitScalar_eighthRoot (z : ℂ) (ring : z ∈ synthesisRing) (unitModulus : ‖z‖ = 1) :
    ∃ m : Fin 8, z = omega ^ m.val := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P85

end

Source

Exact synthesis of multiqubit Clifford+T circuits, arXiv:1212.0506v3, PDF p. 6, Remark 7: unit-modulus ring scalars are eighth roots

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every complex number $z$ belonging to the smallest subring of $\mathbb C$ containing $1/\sqrt2$ and $i$ , if $|z|=1$ , then there exists an integer $m\in\{0,\ldots,7\}$ such that

z=\bigl(e^{i\pi/4}\bigr)^m.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph