Majorana matrices on fermionic Fock space

Abstract

Occupation-space Majoranas satisfy Clifford relations and reverse number parity.

Natural subtraction is truncated at zero. All other divisions are in Real or Complex. Scalar casts retain their target type. Matrix products are operator products, and Matrix.conjTranspose is conjugate transpose. Subtype.val is the value of a density; Equiv.symm applied to CStarMatrix.ofMatrix recovers its ordinary matrix. Assignment N is the occupation basis Fin N → Bool. Implicit Lean mode and dimension arguments may be displayed explicitly. Bracketed Fintype, DecidableEq and Nonempty assumptions are anonymous instance arguments.

Definition 1.1 (The two Majoranas of a mode).

$$\forall N\in Nat,\forall j\in \mathrm{Fin}\left(N\right),\forall b\in Bool,\mathrm{majorana}\left(N,j,b\right)=\mathrm{ite}\left(b,\mathrm{SMul}.\mathrm{smul}\left(\mathrm{Complex}.I,(\mathrm{fullC}\left(N,j\right)-\mathrm{fullC}{\left(N,j\right)}^{\ast })\right),\mathrm{fullC}\left(N,j\right)+\mathrm{fullC}{\left(N,j\right)}^{\ast }\right)$$

Formalization. D5/S3/Quantum/Fermionic/FockMajoranaCarrier.majorana (✓ std3).

Citation. Amir-Reza Negari; Farzin Salek; Zoltán Zimborás; Aram Harrow; Patrick Hayden; Jens Eisert (2026). Approximation theorems for fermionic Gaussian states. DOI: 10.48550/arXiv.2610.01860. URL: https://arxiv.org/abs/2610.01860v1.

Commentary.

From the creation and annihilation operators we define Hermitian Majorana operators by [page 4, equation (11)]: γ₂ⱼ₋₁ = cⱼ + cⱼ†, γ₂ⱼ = i(cⱼ − cⱼ†), j = 1, …, m. Here b=false denotes the first operator and b=true the second. The carrier uses N modes in the fixed increasing order.

Definition 1.2 (Number parity as an operator power).

$$\forall N\in Nat,\mathrm{numberParity}\left(N\right)=\mathrm{NormedSpace}.\exp \left(\mathrm{SMul}.\mathrm{smul}\left(\mathrm{Real}.\mathrm{pi}\cdot \mathrm{Complex}.I,\mathrm{numberOperator}\left(N\right)\right)\right)$$

Formalization. D5/S3/Quantum/Fermionic/FockMajoranaCarrier.numberParity (✓ std3).

Citation. Amir-Reza Negari; Farzin Salek; Zoltán Zimborás; Aram Harrow; Patrick Hayden; Jens Eisert (2026). Approximation theorems for fermionic Gaussian states. DOI: 10.48550/arXiv.2610.01860. URL: https://arxiv.org/abs/2610.01860v1.

Commentary.

“The number operator and parity operator are given by” [printed page 3]: N̂ = ∑ⱼ₌₁ᵐ cⱼ†cⱼ, P = (−1)^N̂. The operator-power convention is P = exp(iπN̂). Its diagonal form follows from the occupation-factor calculation of the number operator.

Definition 1.3 (Number operator).

$$\forall N\in Nat,\mathrm{numberOperator}\left(N\right)=\sum _{j:\mathrm{Fin}\left(N\right)}(\mathrm{fullC}{\left(N,j\right)}^{\ast }\cdot \mathrm{fullC}\left(N,j\right))$$

Formalization. D5/S3/Quantum/Fermionic/FockMajoranaCarrier.numberOperator (✓ std3).

Citation. Amir-Reza Negari; Farzin Salek; Zoltán Zimborás; Aram Harrow; Patrick Hayden; Jens Eisert (2026). Approximation theorems for fermionic Gaussian states. DOI: 10.48550/arXiv.2610.01860. URL: https://arxiv.org/abs/2610.01860v1.

Commentary.

“The number operator and parity operator are given by” [printed page 3]: N̂ = ∑ⱼ₌₁ᵐ cⱼ†cⱼ, P = (−1)^N̂. Here fullC is the Jordan–Wigner annihilator and N counts all global modes.

Theorem 1.4 (Number operator in the occupation basis).

$$\forall N\in Nat,\mathrm{numberOperator}\left(N\right)=\mathrm{Matrix}.\mathrm{diagonal}\left(s:\mathrm{Assignment}\left(N\right)\mapsto (\mathrm{occupationCount}\left(s\right):Complex)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/FockMajoranaCarrier.numberOperator_eq_diagonal (✓ std3). ∎

Citation. Amir-Reza Negari; Farzin Salek; Zoltán Zimborás; Aram Harrow; Patrick Hayden; Jens Eisert (2026). Approximation theorems for fermionic Gaussian states. DOI: 10.48550/arXiv.2610.01860. URL: https://arxiv.org/abs/2610.01860v1.

Commentary.

The explicit occupation-factor calculation identifies the operator sum with the diagonal matrix of the occupied-mode count.

Theorem 1.5 (Number parity in the occupation basis).

$$\forall N\in Nat,\mathrm{numberParity}\left(N\right)=\mathrm{Matrix}.\mathrm{diagonal}\left(s:\mathrm{Assignment}\left(N\right)\mapsto (-(1:Complex){)}^{\mathrm{occupationCount}\left(s\right)}\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/FockMajoranaCarrier.numberParity_eq_diagonal (✓ std3). ∎

Citation. Amir-Reza Negari; Farzin Salek; Zoltán Zimborás; Aram Harrow; Patrick Hayden; Jens Eisert (2026). Approximation theorems for fermionic Gaussian states. DOI: 10.48550/arXiv.2610.01860. URL: https://arxiv.org/abs/2610.01860v1.

Commentary.

The diagonal exponential evaluates to exp(iπ times the integer occupation count), hence to (−1) raised to that count.

Theorem 1.6 (Clifford relations and odd parity).

$$\forall N\in Nat,(\mathrm{Matrix}.\mathrm{IsHermitian}\left(\mathrm{numberParity}\left(N\right)\right))\wedge ((\mathrm{numberParity}\left(N\right)\cdot \mathrm{numberParity}\left(N\right)=(1:\mathrm{FullOperator}\left(N\right)))\wedge ((\forall p\in \mathrm{Prod}\left(\mathrm{Fin}\left(N\right),Bool\right),\mathrm{Matrix}.\mathrm{IsHermitian}\left(\mathrm{majorana}\left(N,\mathrm{Prod}.\mathrm{fst}\left(p\right),\mathrm{Prod}.\mathrm{snd}\left(p\right)\right)\right))\wedge ((\forall p\in \mathrm{Prod}\left(\mathrm{Fin}\left(N\right),Bool\right),\forall q\in \mathrm{Prod}\left(\mathrm{Fin}\left(N\right),Bool\right),\mathrm{majorana}\left(N,\mathrm{Prod}.\mathrm{fst}\left(p\right),\mathrm{Prod}.\mathrm{snd}\left(p\right)\right)\cdot \mathrm{majorana}\left(N,\mathrm{Prod}.\mathrm{fst}\left(q\right),\mathrm{Prod}.\mathrm{snd}\left(q\right)\right)+\mathrm{majorana}\left(N,\mathrm{Prod}.\mathrm{fst}\left(q\right),\mathrm{Prod}.\mathrm{snd}\left(q\right)\right)\cdot \mathrm{majorana}\left(N,\mathrm{Prod}.\mathrm{fst}\left(p\right),\mathrm{Prod}.\mathrm{snd}\left(p\right)\right)=\mathrm{ite}\left(p=q,\mathrm{SMul}.\mathrm{smul}\left((2:Complex),(1:\mathrm{FullOperator}\left(N\right))\right),(0:\mathrm{FullOperator}\left(N\right))\right))\wedge (\forall p\in \mathrm{Prod}\left(\mathrm{Fin}\left(N\right),Bool\right),\mathrm{numberParity}\left(N\right)\cdot \mathrm{majorana}\left(N,\mathrm{Prod}.\mathrm{fst}\left(p\right),\mathrm{Prod}.\mathrm{snd}\left(p\right)\right)+\mathrm{majorana}\left(N,\mathrm{Prod}.\mathrm{fst}\left(p\right),\mathrm{Prod}.\mathrm{snd}\left(p\right)\right)\cdot \mathrm{numberParity}\left(N\right)=(0:\mathrm{FullOperator}\left(N\right))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fermionic/FockMajoranaCarrier.majorana_clifford_and_parity (✓ std3). ∎

Citation. Amir-Reza Negari; Farzin Salek; Zoltán Zimborás; Aram Harrow; Patrick Hayden; Jens Eisert (2026). Approximation theorems for fermionic Gaussian states. DOI: 10.48550/arXiv.2610.01860. URL: https://arxiv.org/abs/2610.01860v1.

Commentary.

They satisfy the Clifford relations [page 4, equation (12)]: {γₚ,γ_q} = 2δₚ,q 1, γₚ† = γₚ. The displayed statement verifies these relations for the actual Jordan–Wigner matrices and also verifies that number parity is a Hermitian involution which anticommutes with each generator. Products of two generators consequently commute with number parity.

References

• Truth anchor: D5/S3/Quantum/Fermionic/FockMajoranaCarrier.majorana
• Truth anchor: D5/S3/Quantum/Fermionic/FockMajoranaCarrier.majorana_clifford_and_parity
• Truth anchor: D5/S3/Quantum/Fermionic/FockMajoranaCarrier.numberOperator
• Truth anchor: D5/S3/Quantum/Fermionic/FockMajoranaCarrier.numberOperator_eq_diagonal
• Truth anchor: D5/S3/Quantum/Fermionic/FockMajoranaCarrier.numberParity
• Truth anchor: D5/S3/Quantum/Fermionic/FockMajoranaCarrier.numberParity_eq_diagonal
• Dependency: D5/S3/Quantum/FockSpace/ForbiddenNeighbourDeterminant
• Dependency: D5/S3/Quantum/SpinChains/SupersymmetricFermion/JordanWigner