Fourier Clifford Vacuum

Abstract

The product of Fourier number projections is a Hermitian idempotent.

Formulas retain Lean application and binder notation. Omega denotes the outcome-index type Ω, whereas ω denotes an outcome. Square brackets denote anonymous typeclass assumptions. Scalar coercions display their target types; angle brackets suppress the proof field of a Fin value. The identity is written as 1. Products of matrices and scalar actions use a centered dot; the operand types distinguish them. Infix Matrix.kronecker denotes the Lean kronecker notation.

Lemma 1.1 (Vanishing self-anticommutator).

$$\begin{array}{r}\forall \{R:\mathrm{Type}\ast \},\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ [\mathrm{StarRing}R],\\ [\mathrm{StarModule}\mathbb{C}R],\\ \forall (b:R),\\ (b\cdot b+b\cdot b=0)\to b\cdot b=0\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.CAR_nilpotent (✓ std3). ∎

Source. Repository-derived.

Commentary.

In a complex algebra with compatible star, a vanishing self-anticommutator forces the square to vanish. Type* allows the algebra to lie in any universe.

Lemma 1.2 (Anticommutator of linear combinations).

$$\forall \{R:\mathrm{Type}{u}_1\},([\mathrm{Ring}\left(R\right)],([\mathrm{Algebra}\left(\mathbb{C},R\right)],(\forall \{\iota :\mathrm{Type}{u}_2\},([\mathrm{Fintype}\left(\iota \right)],([\mathrm{DecidableEq}\left(\iota \right)],(\forall (g:\iota \to R),((\forall (j:\iota ),((g\left(j\right))\cdot (g\left(j\right))=(1:R)))\to ((\forall (j:\iota ),(\forall (k:\iota ),((j\ne k)\to ((g\left(j\right))\cdot (g\left(k\right))=-((g\left(k\right))\cdot (g\left(j\right)))))))\to (\forall (c:\iota \to \mathbb{C}),(\forall (d:\iota \to \mathbb{C}),((Fintype.linearCombination\left(\mathbb{C},g,c\right))\cdot (Fintype.linearCombination\left(\mathbb{C},g,d\right))+(Fintype.linearCombination\left(\mathbb{C},g,d\right))\cdot (Fintype.linearCombination\left(\mathbb{C},g,c\right))=(\mathrm{algebraMap}\left(\mathbb{C},R,(((2:\mathbb{C}))\cdot (\sum _{j:\iota }((c\left(j\right))\cdot (d\left(j\right)))):\mathbb{C})\right))\cdot ((1:R)))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.cliffordLinear_anticommutator (✓ std3). ∎

Source. Repository-derived.

Commentary.

For pairwise anticommuting involutions in a complex algebra, the anticommutator of two linear combinations is twice the bilinear pairing of their coefficients times the identity. The algebra and the index type may lie in independent universes u₁ and u₂. Fintype.linearCombination uses the complex scalar action, and the displayed algebraMap explicitly maps the complex coefficient into R: z • x = algebraMap ℂ R z * x.

Definition 1.3 (averaging).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ \forall (u:R),\\ (\mathrm{averaging}(R:=R)(u:=u):R{\to }_l[\mathbb{C}]R)=((1/2:\mathbb{C})\cdot (\mathrm{LinearMap}.\mathrm{id}+(\mathrm{LinearMap}.\mathrm{mulLeftRight}\mathbb{C}(u,u))))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.averaging (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines averaging.

Definition 1.4 (finiteTwirl).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ \forall (g:\mathbb{N}\to R),\\ \forall (k:\mathbb{N}),\\ (\mathrm{finiteTwirl}(R:=R)(g:=g)(k:=k):R{\to }_l[\mathbb{C}]R)=(((\mathrm{List}.\mathrm{range}k).\mathrm{map}(\mathrm{fun}j\mapsto \mathrm{averaging}(gj))).\mathrm{prod})\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.finiteTwirl (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines finiteTwirl.

Lemma 1.5 (finiteTwirl step).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ \forall (g:\mathbb{N}\to R),\\ \forall (k:\mathbb{N}),\\ \forall (X:R),\\ \mathrm{finiteTwirl}g(k+1)X=(1/2:\mathbb{C})\cdot (\mathrm{finiteTwirl}gkX+\mathrm{finiteTwirl}gk(gk\cdot X\cdot gk))\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.finiteTwirl_step (✓ std3). ∎

Source. Repository-derived.

Commentary.

This finiteTwirl step identity is used in the FourierCliffordVacuum construction.

Definition 1.6 (vacuumWord).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ \forall (p:\mathbb{N}\to R),\\ \forall (k:\mathbb{N}),\\ (\mathrm{vacuumWord}(R:=R)(p:=p)(k:=k):R)=((((\mathrm{List}.\mathrm{range}k).\mathrm{reverse}).\mathrm{map}p).\mathrm{prod})\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.vacuumWord (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines vacuumWord.

Definition 1.7 (cycleFrequency).

$$\begin{array}{r}\forall (L:\mathbb{N}),\\ \forall (r:\mathrm{Fin}L),\\ (\mathrm{cycleFrequency}(L:=L)(r:=r):\mathbb{R})=((2\cdot (r:\mathbb{R})+1)\cdot \mathrm{theta}L)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.cycleFrequency (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines cycleFrequency.

Definition 1.8 (modeScale).

$$\begin{array}{r}\forall (L:\mathbb{N}),\\ (\mathrm{modeScale}(L:=L):\mathbb{C})=(((((\mathrm{Real}.\mathrm{sqrt}((4\cdot L:\mathbb{N}):\mathbb{R})){)}^{-1}:\mathbb{R}):\mathbb{C}))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.modeScale (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines modeScale.

Definition 1.9 (modeCoeff).

$$\begin{array}{r}\forall (L:\mathbb{N}),\\ \forall (r:\mathrm{Fin}L),\\ \forall (j:\mathrm{Fin}(2\cdot L)),\\ (\mathrm{modeCoeff}(L:=L)(r:=r)(j:=j):\mathbb{C})=(\mathrm{modeScale}L\cdot (\mathrm{fun}x:\mathbb{R}\mapsto (\mathrm{Real}.\mathrm{probChar}x:\mathbb{C}))(-(j:\mathbb{R})\cdot \mathrm{cycleFrequency}Lr))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.modeCoeff (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines modeCoeff.

Lemma 1.10 (modeScale star).

$$\begin{array}{r}\forall (L:\mathbb{N}),\\ \mathrm{star}(\mathrm{modeScale}L)=\mathrm{modeScale}L\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.modeScale_star (✓ std3). ∎

Source. Repository-derived.

Commentary.

This modeScale star identity is used in the FourierCliffordVacuum construction.

Lemma 1.11 (modeScale square).

$$\begin{array}{r}\forall (L:\mathbb{N}),\\ (0<L)\to \\ \mathrm{modeScale}L\cdot \mathrm{modeScale}L=(((4\cdot L:\mathbb{N}):\mathbb{C}){)}^{-1}\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.modeScale_square (✓ std3). ∎

Source. Repository-derived.

Commentary.

This modeScale square identity is used in the FourierCliffordVacuum construction.

Definition 1.12 (fourierMode).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ \forall (L:\mathbb{N}),\\ \forall (g:\mathrm{Fin}(2\cdot L)\to R),\\ \forall (r:\mathrm{Fin}L),\\ (\mathrm{fourierMode}(R:=R)(L:=L)(g:=g)(r:=r):R)=(\mathrm{Fintype}.\mathrm{linearCombination}\mathbb{C}g(\mathrm{modeCoeff}Lr))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.fourierMode (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines fourierMode.

Definition 1.13 (totalGamma).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ \forall (L:\mathbb{N}),\\ \forall (g:\mathrm{Fin}(2\cdot L)\to R),\\ \forall (k:\mathbb{N}),\\ (\mathrm{totalGamma}(R:=R)(L:=L)(g:=g)(k:=k):R)=(\mathrm{if}\mathrm{hk}:k<2\cdot L\mathrm{then}g⟨k,\mathrm{hk}⟩\mathrm{else}0)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.totalGamma (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines totalGamma.

Definition 1.14 (cliffordAverage).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ \forall (L:\mathbb{N}),\\ \forall (g:\mathrm{Fin}(2\cdot L)\to R),\\ (\mathrm{cliffordAverage}(R:=R)(L:=L)(g:=g):R{\to }_l[\mathbb{C}]R)=(\mathrm{finiteTwirl}(\mathrm{totalGamma}g)(2\cdot L))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.cliffordAverage (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines cliffordAverage.

Definition 1.15 (totalMode).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ \forall (L:\mathbb{N}),\\ \forall (g:\mathrm{Fin}(2\cdot L)\to R),\\ \forall (k:\mathbb{N}),\\ (\mathrm{totalMode}(R:=R)(L:=L)(g:=g)(k:=k):R)=(\mathrm{if}\mathrm{hk}:k<L\mathrm{then}\mathrm{fourierMode}g⟨k,\mathrm{hk}⟩\mathrm{else}0)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.totalMode (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines totalMode.

Definition 1.16 (numberProjection).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ [\mathrm{StarRing}R],\\ \forall (L:\mathbb{N}),\\ \forall (g:\mathrm{Fin}(2\cdot L)\to R),\\ \forall (k:\mathbb{N}),\\ (\mathrm{numberProjection}(R:=R)(L:=L)(g:=g)(k:=k):R)=(\mathrm{totalMode}gk\cdot \mathrm{star}(\mathrm{totalMode}gk))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.numberProjection (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines numberProjection.

Definition 1.17 (fourierVacuum).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ [\mathrm{StarRing}R],\\ \forall (L:\mathbb{N}),\\ \forall (g:\mathrm{Fin}(2\cdot L)\to R),\\ (\mathrm{fourierVacuum}(R:=R)(L:=L)(g:=g):R)=(\mathrm{vacuumWord}(\mathrm{numberProjection}g)L)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.fourierVacuum (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines fourierVacuum.

Lemma 1.18 (fourierVacuum properties).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ [\mathrm{StarRing}R],\\ [\mathrm{StarModule}\mathbb{C}R],\\ \forall (L:\mathbb{N}),\\ (0<L)\to \\ \forall (g:\mathrm{Fin}(2\cdot L)\to R),\\ (\forall j,gj\cdot gj=1)\to \\ (\forall j,\mathrm{star}(gj)=gj)\to \\ (\forall jk,j\ne k\to gj\cdot gk=-(gk\cdot gj))\to \\ \mathrm{star}(\mathrm{fourierVacuum}g)=\mathrm{fourierVacuum}g\wedge \mathrm{fourierVacuum}g\cdot \mathrm{fourierVacuum}g=\mathrm{fourierVacuum}g\wedge (\forall k,k<L\to \mathrm{totalMode}gk\cdot \mathrm{fourierVacuum}g=0\wedge \mathrm{fourierVacuum}g\cdot \mathrm{star}(\mathrm{totalMode}gk)=0)\wedge \mathrm{cliffordAverage}g(\mathrm{fourierVacuum}g)=(((1/2:\mathbb{C}){)}^L)\cdot (1:R)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.fourierVacuum_properties (✓ std3). ∎

Source. Repository-derived.

Commentary.

The product of Fourier number projections is a Hermitian idempotent. Every Fourier annihilator kills it on the left and its adjoint kills it on the right. Averaging conjugations by all Majoranas gives exactly 2^(−L) times the identity.

Lemma 1.19 (fourierVacuum psd).

$$\begin{array}{r}\forall (\iota :\mathrm{Type}),\\ [\mathrm{Fintype}\iota ],\\ [\mathrm{DecidableEq}\iota ],\\ \forall (L:\mathbb{N}),\\ (0<L)\to \\ \forall (g:\mathrm{Fin}(2\cdot L)\to \mathrm{Matrix}\iota \iota \mathbb{C}),\\ (\forall j,gj\cdot gj=1)\to \\ (\forall j,\mathrm{star}(gj)=gj)\to \\ (\forall jk,j\ne k\to gj\cdot gk=-(gk\cdot gj))\to \\ (\mathrm{fourierVacuum}g).\mathrm{PosSemidef}\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.fourierVacuum_psd (✓ std3). ∎

Source. Repository-derived.

Commentary.

This fourierVacuum psd identity is used in the FourierCliffordVacuum construction.

Lemma 1.20 (fourierVacuum covariance).

$$\begin{array}{r}\forall (R:\mathrm{Type}),\\ [\mathrm{Ring}R],\\ [\mathrm{Algebra}\mathbb{C}R],\\ [\mathrm{StarRing}R],\\ [\mathrm{StarModule}\mathbb{C}R],\\ \forall (L:\mathbb{N}),\\ (0<L)\to \\ \forall (g:\mathrm{Fin}(2\cdot L)\to R),\\ (\forall j,gj\cdot gj=1)\to \\ (\forall j,\mathrm{star}(gj)=gj)\to \\ (\forall jk,j\ne k\to gj\cdot gk=-(gk\cdot gj))\to \\ \forall (j:\mathrm{Fin}(2\cdot L)),\\ \forall (k:\mathrm{Fin}(2\cdot L)),\\ \mathrm{cliffordAverage}g(gj\cdot gk\cdot \mathrm{fourierVacuum}g)=(4\cdot \sum r:\mathrm{Fin}L,\mathrm{star}(\mathrm{modeCoeff}Lrj)\cdot \mathrm{modeCoeff}Lrk)\cdot \mathrm{cliffordAverage}g(\mathrm{fourierVacuum}g)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.fourierVacuum_covariance (✓ std3). ∎

Source. Repository-derived.

Commentary.

This fourierVacuum covariance identity is used in the FourierCliffordVacuum construction.

References

• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.CAR_nilpotent
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.averaging
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.cliffordAverage
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.cliffordLinear_anticommutator
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.cycleFrequency
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.finiteTwirl
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.finiteTwirl_step
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.fourierMode
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.fourierVacuum
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.fourierVacuum_covariance
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.fourierVacuum_properties
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.fourierVacuum_psd
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.modeCoeff
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.modeScale
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.modeScale_square
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.modeScale_star
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.numberProjection
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.totalGamma
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.totalMode
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/FourierCliffordVacuum.vacuumWord
• Dependency: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate