Shifted Fourier Operator Certificate

Abstract

The sine-product weights admit a shifted Fourier reduction to a difference of positive weighted Laplacians.

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 (sine weights path sum).

$$\begin{array}{r}\forall (K:\mathbb{N}),\\ \mathrm{let}\theta :=\mathrm{Real}.\mathrm{pi}/((K+2:\mathbb{N}):\mathbb{R});(\sum j\in \mathrm{Finset}.\mathrm{range}K,\mathrm{Real}.\sin (((j:\mathbb{R})+1)\cdot \theta )\cdot \mathrm{Real}.\sin (((j:\mathbb{R})+2)\cdot \theta ))=((K+2:\mathbb{N}):\mathbb{R})/2\cdot \mathrm{Real}.\cos \theta \end{array}$$

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

Source. Repository-derived.

Commentary.

This sine weights path sum identity is used in the ShiftedFourierOperatorCertificate construction.

Definition 1.2 (theta).

$$\begin{array}{r}\forall (L:\mathbb{N}),\\ (\mathrm{theta}(L:=L):\mathbb{R})=(\mathrm{Real}.\mathrm{pi}/(2\cdot (L:\mathbb{R})))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.theta (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines theta.

Lemma 1.3 (theta pos).

$$\begin{array}{r}\forall (L:\mathbb{N}),\\ (0<L)\to \\ 0<\mathrm{theta}L\end{array}$$

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

Source. Repository-derived.

Commentary.

This theta pos identity is used in the ShiftedFourierOperatorCertificate construction.

Lemma 1.4 (theta mul L).

$$\begin{array}{r}\forall (L:\mathbb{N}),\\ (0<L)\to \\ (L:\mathbb{R})\cdot \mathrm{theta}L=\mathrm{Real}.\mathrm{pi}/2\end{array}$$

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

Source. Repository-derived.

Commentary.

This theta mul L identity is used in the ShiftedFourierOperatorCertificate construction.

Lemma 1.5 (exponential sum orthogonality).

$$\begin{array}{r}\forall (M:\mathbb{N}),\\ (0<M)\to \\ \forall (r:\mathrm{Fin}M),\\ \forall (s:\mathrm{Fin}M),\\ (\sum j\in \mathrm{Finset}.\mathrm{range}M,\mathrm{Complex}.\exp (((2\cdot \mathrm{Real}.\mathrm{pi}\cdot ((r:\mathbb{R})-(s:\mathbb{R}))/(M:\mathbb{R}))\cdot (j:\mathbb{R}):\mathbb{R})\cdot \mathrm{Complex}.I))=\mathrm{if}r=s\mathrm{then}(M:\mathbb{C})\mathrm{else}0\end{array}$$

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

Source. Repository-derived.

Commentary.

This exponential sum orthogonality identity is used in the ShiftedFourierOperatorCertificate construction.

Lemma 1.6 (phase star).

$$\begin{array}{r}\forall (x:\mathbb{R}),\\ \mathrm{star}((\mathrm{fun}x:\mathbb{R}\mapsto (\mathrm{Real}.\mathrm{probChar}x:\mathbb{C}))x)=(\mathrm{fun}x:\mathbb{R}\mapsto (\mathrm{Real}.\mathrm{probChar}x:\mathbb{C}))(-x)\end{array}$$

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

Source. Repository-derived.

Commentary.

This phase star identity is used in the ShiftedFourierOperatorCertificate construction.

Lemma 1.7 (phase mul).

$$\begin{array}{r}\forall (x:\mathbb{R}),\\ \forall (y:\mathbb{R}),\\ (\mathrm{fun}x:\mathbb{R}\mapsto (\mathrm{Real}.\mathrm{probChar}x:\mathbb{C}))x\cdot (\mathrm{fun}x:\mathbb{R}\mapsto (\mathrm{Real}.\mathrm{probChar}x:\mathbb{C}))y=(\mathrm{fun}x:\mathbb{R}\mapsto (\mathrm{Real}.\mathrm{probChar}x:\mathbb{C}))(x+y)\end{array}$$

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

Source. Repository-derived.

Commentary.

This phase mul identity is used in the ShiftedFourierOperatorCertificate construction.

Lemma 1.8 (phase cos).

$$\begin{array}{r}\forall (x:\mathbb{R}),\\ (\mathrm{Real}.\cos x:\mathbb{C})=((\mathrm{fun}x:\mathbb{R}\mapsto (\mathrm{Real}.\mathrm{probChar}x:\mathbb{C}))x+(\mathrm{fun}x:\mathbb{R}\mapsto (\mathrm{Real}.\mathrm{probChar}x:\mathbb{C}))(-x))/2\end{array}$$

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

Source. Repository-derived.

Commentary.

This phase cos identity is used in the ShiftedFourierOperatorCertificate construction.

Definition 1.9 (pathWeight).

$$\begin{array}{r}\forall (L:\mathbb{N}),\\ \forall (j:\mathbb{R}),\\ (\mathrm{pathWeight}(L:=L)(j:=j):\mathbb{R})=((\mathrm{Real}.\cos (\mathrm{theta}L)-\mathrm{Real}.\cos ((2\cdot j+1)\cdot \mathrm{theta}L))/2)\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.pathWeight (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines pathWeight.

Definition 1.10 (pathDualWeight).

$$\begin{array}{r}\forall (n:\mathbb{N}),\\ \forall (k:\mathrm{Fin}(2\cdot n)),\\ (\mathrm{pathDualWeight}(n:=n)(k:=k):\mathbb{R})=(\mathrm{pathWeight}(n+1)((k:\mathbb{R})+1))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.pathDualWeight (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines pathDualWeight.

Definition 1.11 (padCompression).

$$\begin{array}{r}\forall (d:\mathbb{N}),\\ (\mathrm{padCompression}(d:=d):\mathrm{Matrix}((\mathrm{Fin}d\times \mathrm{Fin}2)\times \mathrm{Fin}2)(\mathrm{Fin}d)\mathbb{C})=((\mathrm{qubitV}(\iota :=\mathrm{Fin}d\times \mathrm{Fin}2):\mathrm{Matrix}((\mathrm{Fin}d\times \mathrm{Fin}2)\times \mathrm{Fin}2)(\mathrm{Fin}d\times \mathrm{Fin}2)\mathbb{C})\cdot ((\mathrm{qubitV}(\iota :=\mathrm{Fin}d)):\mathrm{Matrix}(\mathrm{Fin}d\times \mathrm{Fin}2)(\mathrm{Fin}d)\mathbb{C}))\end{array}$$

Formalization. D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.padCompression (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines padCompression.

Lemma 1.12 (padCompression isometry).

$$\begin{array}{r}\forall (d:\mathbb{N}),\\ (\mathrm{padCompression}d).\mathrm{conjTranspose}\cdot \mathrm{padCompression}d=1\end{array}$$

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

Source. Repository-derived.

Commentary.

This padCompression isometry identity is used in the ShiftedFourierOperatorCertificate construction.

Lemma 1.13 (padCompression compress).

$$\begin{array}{r}\forall (d:\mathbb{N}),\\ \forall (B:(\mathrm{Matrix}(\mathrm{Fin}d\times \mathrm{Fin}2)(\mathrm{Fin}d\times \mathrm{Fin}2)\mathbb{C})),\\ (\mathrm{padCompression}d).\mathrm{conjTranspose}\cdot (B(\mathrm{Matrix}.\mathrm{kronecker})(1:\mathrm{Matrix}(\mathrm{Fin}2)(\mathrm{Fin}2)\mathbb{C}))\cdot \mathrm{padCompression}d=((\mathrm{qubitV}(\iota :=\mathrm{Fin}d))).\mathrm{conjTranspose}\cdot B\cdot (\mathrm{qubitV}(\iota :=\mathrm{Fin}d))\end{array}$$

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

Source. Repository-derived.

Commentary.

This padCompression compress identity is used in the ShiftedFourierOperatorCertificate construction.

Lemma 1.14 (pathWeight sine).

$$\begin{array}{r}\forall (L:\mathbb{N}),\\ \forall (j:\mathbb{R}),\\ \mathrm{pathWeight}Lj=\mathrm{Real}.\sin (j\cdot \mathrm{theta}L)\cdot \mathrm{Real}.\sin ((j+1)\cdot \mathrm{theta}L)\end{array}$$

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

Source. Repository-derived.

Commentary.

This pathWeight sine identity is used in the ShiftedFourierOperatorCertificate construction.

Lemma 1.15 (path dual operator certificate).

$$\begin{array}{r}\forall (n:\mathbb{N}),\\ \forall (d:\mathbb{N}),\\ (1\le n)\to \\ \forall (A:\mathrm{Fin}(2\cdot n)\to (\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\\ (\mathrm{Realization}(\mathrm{SimpleGraph}.\mathrm{pathGraph}(2\cdot n))A)\to \\ \forall (a:\mathrm{Fin}(2\cdot n)\to \mathrm{Bool}),\\ (((\mathrm{Real}.\cos (\mathrm{theta}(n+1))/\mathrm{Real}.\sin (\mathrm{theta}(n+1)):\mathbb{C}))\cdot (1:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))-\mathrm{weightedHamiltonian}A(\mathrm{pathDualWeight}n)a).\mathrm{PosSemidef}\end{array}$$

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

Source. Repository-derived.

Commentary.

The sine-product weights admit a shifted Fourier reduction to a difference of positive weighted Laplacians. Its positive trace is cot(theta (n+1)). The Majorana quadratic bound and the ancilla compression give this operator inequality for every path realization and every Boolean outcome.

Lemma 1.16 (visibility as L).

$$\begin{array}{r}\forall (n:\mathbb{N}),\\ \mathrm{visibility}n=1/(((n+1:\mathbb{N}):\mathbb{R})\cdot \mathrm{Real}.\sin (\mathrm{theta}(n+1)))\end{array}$$

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

Source. Repository-derived.

Commentary.

This visibility as L identity is used in the ShiftedFourierOperatorCertificate construction.

Lemma 1.17 (visibility Icc).

$$\begin{array}{r}\forall (n:\mathbb{N}),\\ (1\le n)\to \\ \mathrm{visibility}n\in \mathrm{Set}.\mathrm{Icc}(0:\mathbb{R})1\end{array}$$

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

Source. Repository-derived.

Commentary.

This visibility Icc identity is used in the ShiftedFourierOperatorCertificate construction.

Lemma 1.18 (visibility upper of weighted).

$$\begin{array}{r}\forall (n:\mathbb{N}),\\ (1\le n)\to \\ \forall (t:\mathbb{R}),\\ (t\cdot (((n+1:\mathbb{N}):\mathbb{R})\cdot \mathrm{Real}.\cos (\mathrm{theta}(n+1)))\le \mathrm{Real}.\cos (\mathrm{theta}(n+1))/\mathrm{Real}.\sin (\mathrm{theta}(n+1)))\to \\ t\le \mathrm{visibility}n\end{array}$$

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

Source. Repository-derived.

Commentary.

This visibility upper of weighted identity is used in the ShiftedFourierOperatorCertificate construction.

References

• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.exponential_sum_orthogonality
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.padCompression
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.padCompression_compress
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.padCompression_isometry
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.pathDualWeight
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.pathWeight
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.pathWeight_sine
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.path_dual_operator_certificate
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.phase_cos
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.phase_mul
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.phase_star
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.sine_weights_path_sum
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.theta
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.theta_mul_L
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.theta_pos
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.visibility_Icc
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.visibility_as_L
• Truth anchor: D5/S3/Quantum/Measurements/CliffordJointMeasurability/ShiftedFourierOperatorCertificate.visibility_upper_of_weighted
• Dependency: D5/S3/Quantum/Dynamics/PolygonalFourierCouplings
• Dependency: D5/S3/Quantum/Measurements/CliffordJointMeasurability/CliffordPathRealizations