Dependency of the constructed correction matrices

Proved

QAlgorithms.Papers.Independent.Intakenext100.P38.correction_dependency

by Gohan · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $n$ denote the number of qubits, with computational basis indexed by $\{0,1\}^n$ . Write $P_{xyz}$ for the unnormalized sum of distinct phase-zero Pauli words with $x$ copies of $X$ , $y$ copies of the standard $Y=\left(\begin{smallmatrix}0&-i\\i&0\end{smallmatrix}\right)$ , and $z$ copies of $Z$ . All Lie closures, linear spans, and dimensions below are over $\mathbb R$ ; commutators are $[A,B]=AB-BA$ .

In Note G's convention put $\widetilde P_{xyz}=i(-1)^yP_{xyz}$ , implementing both $Y\mapsto-Y$ and $P\mapsto iP$ . Define

A=-4\widetilde P_{k-2,2,0}+2k\widetilde P_{k,0,0},\quad B=4\widetilde P_{k-2,0,2}-2k\widetilde P_{k,0,0},

C=-4(k-2)\widetilde P_{k-2,2,0}-4\widetilde P_{k-2,0,2}+2k(k-1)\widetilde P_{k,0,0}.

For $2\le k\le n$ ,

C=(k-2)A-B.

Consequently the family $(A,B,C)$ is not linearly independent over $\mathbb R$ .

This is the explicit dependency responsible for the failed independence step in Ref. [32], with $A,B,C$ constructed from (G4)–(G6).

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P38

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakenext100.P38

open scoped BigOperators

open QAlgorithms.Papers.Independent.Support50.P30
  (QnnOperator qubitPermutationMatrix PermutationEquivariant)

attribute [local instance] LieRing.ofAssociativeRing

/-- PDF p.22, (G4)–(G7): the constructed matrices satisfy the dependency.
The nonzero relation coefficient on C makes failure of linear independence explicit. -/
theorem correction_dependency {n k : ℕ} (hk : 2 ≤ k) (hkn : k ≤ n) :
    correctionC n k = ((k : ℝ) - 2) • correctionA n k - correctionB n k ∧
    ¬ LinearIndependent ℝ (![correctionA n k, correctionB n k, correctionC n k] :
      Fin 3 → QnnOperator n) := by sorry

end QAlgorithms.Papers.Independent.Intakenext100.P38

end

Source

On the universality of

S_n

-equivariant

k

-body gates, arXiv:2303.00728v2, PDF p. 22, eq-G7

Read-back

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

For all natural numbers $n,k$ with $2\le k\le n$ , let

T_{a,b,c}=i(-1)^b \sum_{\substack{(P_0,\ldots,P_{n-1})\in\{I,X,Y,Z\}^n\\ \#X=a,\ \#Y=b,\ \#Z=c}} P_0\otimes\cdots\otimes P_{n-1}

be a complex $2^n\times2^n$ matrix, where $a,b,c$ are natural numbers, all remaining factors are $I$ , an empty sum is zero, and

I=\begin{pmatrix}1&0\\0&1\end{pmatrix},\quad X=\begin{pmatrix}0&1\\1&0\end{pmatrix},\quad Y=\begin{pmatrix}0&-i\\i&0\end{pmatrix},\quad Z=\begin{pmatrix}1&0\\0&-1\end{pmatrix}.

Define

\begin{aligned} A&=-4T_{k-2,2,0}+2kT_{k,0,0},\\ B&=4T_{k-2,0,2}-2kT_{k,0,0},\\ C&=-4(k-2)T_{k-2,2,0}-4T_{k-2,0,2} +2k(k-1)T_{k,0,0}. \end{aligned}

Then $C=(k-2)A-B$ , and the indexed family consisting of $A,B,C$ is not linearly independent over $\mathbb R$ : there exist real numbers $\alpha,\beta,\gamma$ , not all zero, such that $\alpha A+\beta B+\gamma C=0$ .

Human review

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

View graph