Section 4.1, unnumbered: dihedral quotient (phase typo corrected)

Proved

QAlgorithms.Papers.Independent.Gap48.P12.ct_dihedral_quotient

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

prove2quantum

Let $C_T(C_1)=\{TgT^{-1}:g,TgT^{-1}\in C_1\}$ for the exact Clifford group $C_1$ . With the source's scalar typo corrected, put

K=\{e^{i\pi k/4}I: k=0,1,\ldots,7\}.

Then $K$ is the scalar normal subgroup of $C_T(C_1)$ , and

C_T(C_1)/K\cong D_4,

where $D_4$ is the order-eight symmetry group of a square. The Lean statement identifies the carrier of the constructed ambient subgroup and the carrier of its constructed normal kernel before asserting a multiplicative isomorphism. The printed denominator $8$ would give a set that is not closed; denominator $4$ agrees with the exact symbolic generator $(HP^3)^3=e^{-i\pi/4}I$ . This correction requires independent moderation.

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: quotient by the scalar subgroup is D₄ (order eight).
Printed: K={exp(i*pi*k/8) I : k=0,...,7}; changed: denominator 4.
Why: the printed set omits the eighth power -I of its generator and is not
a subgroup. The corrected roots agree with (H P^3)^3=exp(-i*pi/4) I and
the stated orders 64 and 8. Carrier equalities are conclusions, so neither
subgroup closure nor the scalar correction is smuggled in as a hypothesis.
Independent moderation of this source correction is required. -/
theorem ct_dihedral_quotient :
    (ctGroup : Set (Matrix.unitaryGroup Bool ℂ)) = {u : Matrix.unitaryGroup Bool ℂ | (u : Mat) ∈ ctSet} ∧
    (∀ g : ctGroup, g ∈ scalarKernel ↔ ∃ k : Fin 8,
      (((g : ctGroup) : Matrix.unitaryGroup Bool ℂ) : Mat) = scalarRoot k) ∧
    Nonempty ((ctGroup ⧸ scalarKernel) ≃* DihedralGroup 4) := 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: dihedral quotient (phase typo corrected)

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)$ , $T=\operatorname{diag}(1,e^{i\pi/4})$ , let $\mathcal C$ be the set of matrix values of all finite words over $H,P$ , including the empty word, and define $\mathcal S=\{TcT^\dagger:c\in\mathcal C,\ TcT^\dagger\in\mathcal C\}$ . Let $G$ be the smallest subgroup of $U(2)$ containing every unitary matrix whose underlying matrix lies in $\mathcal S$ , and let $N$ be the smallest normal subgroup of $G$ containing every element of $G$ whose underlying matrix equals $e^{i\pi k/4}I$ for some integer $k\in\{0,\ldots,7\}$ . Three assertions hold together: the underlying set of $G$ is exactly the unitary matrices whose underlying matrices belong to $\mathcal S$ ; for every $g\in G$ ,

g\in N\quad\Longleftrightarrow\quad \text{the underlying matrix of }g=e^{i\pi k/4}I \text{ for some }k\in\{0,\ldots,7\};

and there exists a group isomorphism from $G/N$ to the dihedral group of order $8$ , equivalently the group presented by $\langle r,s\mid r^4=1,\ s^2=1,\ srs=r^{-1}\rangle$ .

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