Fact 1: three Clifford cosets, each of order 64

Proved

QAlgorithms.Papers.Independent.Gap48.P12.clifford_three_cosets

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

prove2quantum

Let $C_1=\langle H,P\rangle$ and $A=C_T(C_1)$ , with exact phase-inclusive matrices. For a matrix $S$ , write $SA=\{Sa:a\in A\}$ . Then

C_1=A\mathbin{\dot\cup}HA\mathbin{\dot\cup}PHA,\qquad |A|=|HA|=|PHA|=64.

Each set is finite and the three sets are pairwise disjoint. The plus signs printed in Fact 1 mean this partition into left cosets. This partition supplies the three choices of left prefix in the rewrite rule.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Gap48_P12

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Gap48.P12

local notation "Mat" => Matrix Bool Bool ℂ

local notation "Vec" => EuclideanSpace ℂ Bool

local notation "wordMatrix" => fun (B : CircuitBasis) (w : CircuitWord) =>
  QAlgorithms.Papers.Independent.Next46.P21.wordMatrix (chronologicalInstructions B w)

/-- PDF p.7, Fact 1 and its following sentence: a disjoint union of
three left cosets, each with exactly 64 distinct exact matrices. -/
theorem clifford_three_cosets :
    cliffordSet .hp = ctSet ∪ leftCoset hadamard ∪ leftCoset (phaseS * hadamard) ∧
    Disjoint ctSet (leftCoset hadamard) ∧
    Disjoint ctSet (leftCoset (phaseS * hadamard)) ∧
    Disjoint (leftCoset hadamard) (leftCoset (phaseS * hadamard)) ∧
    ctSet.Finite ∧ ctSet.ncard = 64 ∧
    (leftCoset hadamard).Finite ∧ (leftCoset hadamard).ncard = 64 ∧
    (leftCoset (phaseS * hadamard)).Finite ∧
      (leftCoset (phaseS * hadamard)).ncard = 64 := by sorry

end QAlgorithms.Papers.Independent.Gap48.P12

end

Source

Representation of Quantum Circuits with Clifford and

π/8

Gates, arXiv:0806.3834v1, PDF p. 7, Fact 1: three Clifford cosets, each of order 64

Read-back

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

Let $\mathrm{Mat}$ be the complex $2\times2$ matrices, with rows and columns ordered as $\mathrm{false},\mathrm{true}$ , and put $H=\frac1{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ , $P=\operatorname{diag}(1,i)$ , and $T=\operatorname{diag}(1,e^{i\pi/4})$ . For a finite word $w$ in the letters $H,P,T$ , let $M(w)$ be the product of its gate matrices in written order, with $M(\varnothing)=I$ . Define $\mathcal C$ to be the set of matrices $M(w)$ for words containing no $T$ , and define $\mathcal D=\{TgT^\dagger:g\in\mathcal C,\ TgT^\dagger\in\mathcal C\}$ , where $\dagger$ denotes conjugate transpose. Then $\mathcal C=\mathcal D\cup H\mathcal D\cup(PH)\mathcal D$ , where $S\mathcal D=\{SV:V\in\mathcal D\}$ ; the three displayed sets are pairwise disjoint; and each of $\mathcal D$ , $H\mathcal D$ , and $(PH)\mathcal D$ is finite and has exactly $64$ elements.

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