Section 4.1, unnumbered: generators of C_T(C_1)

Proved

QAlgorithms.Papers.Independent.Gap48.P12.ct_generators

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

prove2quantum

For the exact Clifford group $C_1=\langle H,P\rangle$ and the image-defined subgroup $C_T(C_1)$ on page 7,

C_T(C_1)=\langle P,\ HP^2H,\ (HP^3)^3\rangle.

These are exact matrix groups. The symbolic third generator evaluates to $e^{-i\pi/4}I$ ; the following printed display $e^{i\pi/8}I$ is erroneous. Keeping the symbolic word preserves the asserted group and its global phases. The result identifies the generators used by the local rewrite construction.

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, §4.1: the printed symbolic generator assertion.
Source discrepancy: the following “namely” display prints exp(i*pi/8) I;
the word (H P^3)^3 actually equals exp(-i*pi/4) I. We retain the symbolic
word and exact phases; independent moderation of the correction is required. -/
theorem ct_generators :
    (generatedCT : Set (Matrix.unitaryGroup Bool ℂ)) = {u : Matrix.unitaryGroup Bool ℂ | (u : Mat) ∈ ctSet} := 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, Section 4.1, unnumbered: generators of C_T(C_1)

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}$ , $P=\operatorname{diag}(1,i)$ , and $T=\operatorname{diag}(1,e^{i\pi/4})$ . Let $\mathcal C$ consist of the matrix values of all finite words over $H,P$ , including $I$ , and set

\mathcal S=\{TcT^\dagger:c\in\mathcal C\ \text{and}\ TcT^\dagger\in\mathcal C\}.

The subgroup of the unitary group $U(2)$ generated by the three matrices $P$ , $HP^2H$ , and $(HP^3)^3$ has, as its underlying set, exactly the unitary matrices whose underlying complex matrices belong to $\mathcal S$ . Here “generated” means the smallest subgroup containing those three matrices, so its elements are finite products of those generators and their inverses, including the empty product.

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