Remark 4.2: Bloch Clifford characterization

Proved

QAlgorithms.Papers.Independent.Gap48.P10.bloch_clifford_characterization

by Goku · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Write $\widehat U$ for the Bloch matrix determined in ordered $X,Y,Z$ coordinates by conjugation $A\mapsto UAU^\dagger$ , and let $\widehat{\mathcal C}$ be the image of the exact Clifford group. Then

|\widehat{\mathcal C}|=24,\qquad \widehat{\mathcal C}=\{R\in SO(3):R_{ij}\in\{-1,0,1\}\} =\{R\in SO(3):R(Q)=Q\},

where $Q=\{x\in\mathbb R^3:-1\le x_i\le1\text{ for all }i\}$ . Here $SO(3)$ means real orthogonal $3\times3$ matrices of determinant one.

The characterization concerns rotational cube symmetries; reflections are excluded by determinant one.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Gap48_P10

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Gap48.P10

open scoped Classical BigOperators Pointwise

open QAlgorithms.Papers.Independent.Next46.P21 (Letter letterMatrix)

open QAlgorithms.QubitChannels (sigma)

-- Equation (1), PDF p.1: notation for Mathlib matrices, without a new declaration.

local notation "Mat" => Matrix Bool Bool ℂ

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

/-- Remark 4.2, PDF p.3. The Bloch Clifford group consists of 24 signed permutation
rotations and is exactly the rotation group preserving the displayed cube. -/
theorem bloch_clifford_characterization :
    Nat.card {V : RealMat // ∃ C : Clifford, operatorBloch C.val = V} = 24 ∧
    ∀ U : RealMat,
      ((∃ C : Clifford, operatorBloch C.val = U) ↔
        SpecialOrthogonal U ∧ ∀ i j, U i j = -1 ∨ U i j = 0 ∨ U i j = 1) ∧
      ((∃ C : Clifford, operatorBloch C.val = U) ↔
        SpecialOrthogonal U ∧ Set.image (fun x => U.mulVec x) cube = cube) := by sorry

end QAlgorithms.Papers.Independent.Gap48.P10

end

Source

Remarks on Matsumoto and Amano's normal form for single-qubit Clifford+T operators, arXiv:1312.6584v2, PDF p. 3, Remark 4.2: Bloch Clifford characterization

Read-back

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

Let $H=\frac1{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ , $S=\operatorname{diag}(1,i)$ , and $\omega=e^{i\pi/4}$ , and let a Clifford matrix be any product in list order of a finite word over $H,S,\omega I$ , including the empty product. Use Boolean matrix indices in the order false, true, and let

\sigma_0=\begin{pmatrix}0&1\\1&0\end{pmatrix},\qquad \sigma_1=\begin{pmatrix}0&-i\\i&0\end{pmatrix},\qquad \sigma_2=\begin{pmatrix}1&0\\0&-1\end{pmatrix}.

For a complex $2\times2$ matrix $C$ , define the real $3\times3$ matrix $B(C)$ by $B(C)_{ij}=\frac12\operatorname{Re}\operatorname{tr}(\sigma_iC\sigma_jC^*)$ , where $C^*$ is the conjugate transpose. The declaration asserts that the set of distinct real matrices $B(C)$ arising from Clifford matrices has cardinality $24$ , and that for every real $3\times3$ matrix $U$ , both of the following equivalences hold: $U=B(C)$ for some Clifford matrix $C$ if and only if $U^{\mathsf T}U=I$ , $UU^{\mathsf T}=I$ , $\det U=1$ , and every entry of $U$ equals $-1$ , $0$ , or $1$ ; and $U=B(C)$ for some Clifford matrix $C$ if and only if those same three orthogonality and determinant identities hold and $\{Ux:x\in[-1,1]^3\}=[-1,1]^3$ .

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by Goku · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph