Quadratic amplitudes and the graph form of stabilizer states

Abstract

Binary quadratic phases describe graph states. A Pauli stabilizer line can be put in this form by single-qubit unitaries.

Lemma 1.1 (The sign of the binary representative).

$$\forall (a:\mathrm{ZMod}\left(2\right)),\mathrm{complexSign}\left(a\right)=(-1:\mathbb{C}{)}^{(a).val}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/BinaryStabilizerGraphNormalForm.complex_sign_val (✓ std3). ∎

Source. Repository-derived.

Commentary.

The complexSign value is −1 raised to the natural representative of a binary residue.

Definition 1.2 (The binary graph amplitude).

$$\forall (N:\mathbb{N}),\forall (\Gamma :\mathrm{Matrix}\left(\mathrm{Fin}\left(N\right),\mathrm{Fin}\left(N\right),\mathrm{ZMod}\left(2\right)\right)),\forall (x:(\mathrm{Fin}\left(N\right)\to \mathrm{Fin}\left(2\right))),\mathrm{graphAmp}\left(\Gamma ,x\right)=(-1:\mathbb{C}{)}^{(\mathrm{normalExponent}\left(\Gamma ,(x:(\mathrm{Fin}\left(N\right)\to \mathrm{ZMod}\left(2\right)))\right)).val}$$

Formalization. D5/S3/Quantum/Information/BinaryStabilizerGraphNormalForm.graphAmp (✓ std3).

Citation. M. Van den Nest, J. Dehaene, B. De Moor (2004). Graphical description of the action of local Clifford transformations on graph states. DOI: 10.1103/PhysRevA.69.022316. URL: https://arxiv.org/abs/quant-ph/0308151v2.

Commentary.

Each edge contributes its binary quadratic monomial. The ordered upper-triangular sum is normalExponent; graphAmp is the complexSign value of that exponent, equivalently −1 raised to its natural representative. This definition accepts every binary matrix, without a symmetry or diagonal hypothesis.

Theorem 1.3 (A graph amplitude for every stabilizer line).

$$\forall (N:\mathbb{N}),\forall (\psi :((\mathrm{Fin}\left(N\right)\to \mathrm{Fin}\left(2\right))\to \mathbb{C})),\mathrm{StabilizedBy}\left(pauliSet,\psi \right)\Rightarrow (\exists (U:(\mathrm{Fin}\left(N\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))),\exists (\Gamma :\mathrm{Matrix}\left(\mathrm{Fin}\left(N\right),\mathrm{Fin}\left(N\right),\mathrm{ZMod}\left(2\right)\right)),\exists (c:\mathbb{C}),(\forall (i:\mathrm{Fin}\left(N\right)),U\left(i\right)\in \mathrm{unitaryGroup}\left(\mathrm{Fin}\left(2\right),\mathbb{C}\right))\wedge ((\Gamma ).IsSymm\wedge ((\forall (i:\mathrm{Fin}\left(N\right)),\Gamma (i,i)=0)\wedge (\psi =SMul.\mathrm{smul}\left(c,(\mathrm{tensorOp}\left(U\right){\ast }_v\mathrm{graphAmp}\left(\Gamma \right))\right)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/BinaryStabilizerGraphNormalForm.stabilizer_graph_normal_form (✓ std3). ∎

Citation. M. Van den Nest, J. Dehaene, B. De Moor (2004). Graphical description of the action of local Clifford transformations on graph states. DOI: 10.1103/PhysRevA.69.022316. URL: https://arxiv.org/abs/quant-ph/0308151v2.

Commentary.

The Pauli stabilizers of a nonzero common eigenline span a binary Lagrangian subspace. Coordinate swaps and a diagonal shear express that subspace as the graph of a symmetric matrix with zero diagonal. Hadamard and phase gates implement these transformations, and Pauli signs identify the remaining line with the quadratic amplitude. Taking the inverse gates gives the unitaries U and the scalar c in the displayed equation; SMul.smul denotes scalar action on the amplitude vector.

References

• Truth anchor: D5/S3/Quantum/Information/BinaryStabilizerGraphNormalForm.complex_sign_val
• Truth anchor: D5/S3/Quantum/Information/BinaryStabilizerGraphNormalForm.graphAmp
• Truth anchor: D5/S3/Quantum/Information/BinaryStabilizerGraphNormalForm.stabilizer_graph_normal_form
• Dependency: D5/S3/Quantum/Information/BinaryLagrangianGraphForm
• Dependency: D5/S3/Quantum/Information/BinaryStabilizerLocalInequivalence
• Dependency: D5/S3/VertexAlgebra/LatticeTwistedGroundRealization