by Goku · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)
prove2quantum
Let (Aj,i,Bj,i) denote the literal input/tail word pairs transcribed from Table j+1, for j=0,1,2 and i=0,…,63, in row order interleaved across the two printed columns. Put S0=I, S1=H, and S2=PH. Each table has exactly 64 entries, and every entry satisfies
fu(Aj,i)T=SjTfu(Bj,i).
The 192 matrices fu(Aj,i) are pairwise distinct and cover exactly C1. The caption correspondences also hold:
The input correspondences are matrix equalities allowing Clifford simplification; they do not assert literal prefix-string equality. The symbol I is transcribed as the empty word. This is the source's complete concrete one-T rewrite interface.
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 and Appendix pp.15–17, Tables 1–3: every literal rule,
64 rows per table, complete nonrepeating Clifford coverage, and both
caption correspondences. The input-prefix correspondences are matrix
equalities, allowing Clifford word simplification. -/
theorem appendix_rewrite_tables :
(∀ j : Fin 3, (appendixTable j).length = 64 ∧ ∀ i : Fin 64,
wordMatrix .hp (appendixRow j i).1 * gateT =
wordMatrix .hp (appendixPrefix j) * gateT * wordMatrix .hp (appendixRow j i).2) ∧
(rewriteTable.map fun row => wordMatrix .hp row.1).Nodup ∧
(∀ U : Mat, U ∈ cliffordSet .hp ↔
U ∈ (rewriteTable.map fun row => wordMatrix .hp row.1)) ∧
(∀ i : Fin 64,
wordMatrix .hp (appendixRow 1 i).1 = hadamard * wordMatrix .hp (appendixRow 0 i).1 ∧
wordMatrix .hp (appendixRow 2 i).1 = phaseS * hadamard * wordMatrix .hp (appendixRow 0 i).1 ∧
(appendixRow 1 i).2 = (appendixRow 0 i).2 ∧
(appendixRow 2 i).2 = (appendixRow 0 i).2) := by sorry
end QAlgorithms.Papers.Independent.Gap48.P12
end
Source
Representation of Quantum Circuits with Clifford and π/8 Gates, arXiv:0806.3834v1, PDF p. 15, Appendix, Tables 1–3: the 192 concrete rewriting rules
Read-back
What the Lean code literally says, in plain math · gpt-6.1-sol
Let
H=21(111−1),P=(100i),T=(100eiπ/4).
For a word w over H,P,T, let W(w) be the product of its letter matrices in the written order, with W(ε)=I for the empty word ε. Let C be the set of matrices W(w) for words containing no T. The three fixed tables of word pairs can be specified by the following 64 triples (ai,ci,bi), in row order starting at i=0; a displayed string denotes its sequence of letters and ε denotes the empty string:
Define r(a) by removing the initial H if a begins with H, and otherwise prefixing H. Table 0 consists of (ai,bi), table 1 of (r(ai),bi), and table 2 of (ci,bi). Write their rows as (uj,i,vj,i), and set p0=ε, p1=H, and p2=PH. Row extraction has the default value (ε,ε) if its index exceeds the list, although the asserted lengths make that default unused for the quantified indices. The declaration asserts jointly that each table has length 64, and that, for every j∈{0,1,2} and every i∈{0,…,63},
W(uj,i)T=W(pj)TW(vj,i);
that the list of matrices obtained by concatenating the evaluated first columns of tables 0,1,2, in that order, contains no duplicates; that, for every complex 2×2 matrix U, membership U∈C is equivalent to occurrence in that concatenated list; and that, for every i∈{0,…,63},
Confirmed by the moderator at approval.