Polygonal couplings and the discrete Fourier transform

Abstract

The polygonal coupling model uses real symmetric circulant matrices with zero diagonal. Diagonal phase shifts act before and after the Hamiltonian evolution.

Definition 1.1 (The normalized Fourier transform on ZMod).

$$\forall N\in \mathbb{N},[\mathrm{NeZero}\left(N\right)],\forall j\in \mathrm{ZMod}\left(N\right),\forall k\in \mathrm{ZMod}\left(N\right),\mathrm{transform}\left(N,j,k\right)=\frac{\mathrm{ZMod}.\mathrm{stdAddChar}\left(-((j)\cdot (k))\right)}{\mathrm{Complex}.\mathrm{ofReal}\left(\mathrm{Real}.\mathrm{sqrt}\left((N:\mathbb{R})\right)\right)}$$

Formalization. D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.transform (✓ std3).

Source. Repository-derived.

Commentary.

For a nonzero modulus, each matrix entry is the standard additive character of the negative product of its two residue indices, divided by the square root of the modulus.

Definition 1.2 (The discrete Fourier eigenvalue).

$$\forall N\in \mathbb{N},[\mathrm{NeZero}\left(N\right)],\forall b\in \mathrm{ZMod}\left(N\right)\to \mathbb{C},\forall k\in \mathrm{ZMod}\left(N\right),\mathrm{spectralValue}\left(N,b,k\right)=\mathrm{ZMod}.\mathrm{dft}\left(b,k\right)$$

Formalization. D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.spectralValue (✓ std3).

Source. Repository-derived.

Commentary.

The eigenvalue at a residue is the discrete Fourier transform of the circulant’s first column at that residue.

Theorem 1.3 (Unitarity of the normalized Fourier transform).

$$\forall N\in \mathbb{N},[\mathrm{NeZero}\left(N\right)],(\mathrm{transform}\left(N\right))\cdot (\mathrm{Matrix}.\mathrm{conjTranspose}\left(\mathrm{transform}\left(N\right)\right))=1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.transform_unitary (✓ std3). ∎

Source. Repository-derived.

Commentary.

Multiplying the Fourier transform by its conjugate transpose gives the identity matrix.

Theorem 1.4 (Diagonalization of a circulant).

$$\forall N\in \mathbb{N},[\mathrm{NeZero}\left(N\right)],\forall b\in \mathrm{ZMod}\left(N\right)\to \mathbb{C},(\mathrm{transform}\left(N\right))\cdot (\mathrm{Matrix}.\mathrm{circulant}\left(b\right))=(\mathrm{Matrix}.\mathrm{diagonal}\left(\mathrm{spectralValue}\left(N,b\right)\right))\cdot (\mathrm{transform}\left(N\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.circulant_spectral (✓ std3). ∎

Source. Repository-derived.

Commentary.

The normalized Fourier transform intertwines a circulant with the diagonal matrix of its discrete Fourier eigenvalues.

Definition 1.5 (The Fourier matrix).

$$\forall N\in \mathbb{N},\forall j\in \mathrm{Fin}\left(N\right),\forall k\in \mathrm{Fin}\left(N\right),(\mathrm{fourier}\left(N\right){)}_{j,k}=\frac{\exp \left(\frac{-(((((2)\cdot (\pi ))\cdot (i))\cdot (j))\cdot (k))}{N}\right)}{\mathrm{sqrt}\left(N\right)}$$

Formalization. D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.fourier (✓ std3).

Citation. Edgar Barriga et al. (2026). N-dimensional discrete Fourier transform via bosonic Hamiltonian. URL: https://arxiv.org/abs/2609.05644.

Commentary.

The indices are the residues represented by 0 through N - 1. The Fourier matrix uses the negative exponential convention and the normalization by the square root of N.

Definition 1.6 (Diagonal phase shifts).

$$\forall N\in \mathbb{N},\forall Phi\in \mathrm{Matrix}\left(\mathrm{Fin}\left(N\right),\mathrm{Fin}\left(N\right),\mathbb{C}\right),\mathrm{IsUnimodularDiagonal}\left(Phi\right)\iff (\exists z\in (\mathrm{Fin}\left(N\right)\to \mathbb{C}),(\forall x\in \mathrm{Fin}\left(N\right),\mathrm{norm}\left(z\left(x\right)\right)=1)\wedge (Phi=\mathrm{diagonal}\left(z\right)))$$

Formalization. D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.IsUnimodularDiagonal (✓ std3).

Citation. Edgar Barriga et al. (2026). N-dimensional discrete Fourier transform via bosonic Hamiltonian. URL: https://arxiv.org/abs/2609.05644.

Commentary.

A diagonal phase matrix has an entry of modulus one at every index.

Definition 1.7 (Polygonal coupling matrices).

$$\forall N\in \mathbb{N},(\neg (N=0))\Rightarrow (\forall C\in \mathrm{Matrix}\left(\mathrm{Fin}\left(N\right),\mathrm{Fin}\left(N\right),\mathbb{R}\right),\mathrm{IsPolygonalCoupling}\left(C\right)\iff (\exists c\in (\mathrm{Fin}\left(N\right)\to \mathbb{R}),(c\left(0\right)=0)\wedge ((\forall l\in \mathrm{Fin}\left(N\right),c\left(-(l)\right)=c\left(l\right))\wedge (\forall i\in \mathrm{Fin}\left(N\right),\forall j\in \mathrm{Fin}\left(N\right),(C{)}_{i,j}=c\left((j)-(i)\right)))))$$

Formalization. D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.IsPolygonalCoupling (✓ std3).

Citation. Edgar Barriga et al. (2026). N-dimensional discrete Fourier transform via bosonic Hamiltonian. URL: https://arxiv.org/abs/2609.05644.

Commentary.

The coupling between i and j depends on j - i modulo N. Reversing this residue preserves the coupling, and the zero residue has zero coupling.

Definition 1.8 (The polygonal Fourier question).

$$claim\iff (\forall N\in \mathbb{N},(\neg (N=0))\Rightarrow (\exists C\in \mathrm{Matrix}\left(\mathrm{Fin}\left(N\right),\mathrm{Fin}\left(N\right),\mathbb{R}\right),(\mathrm{IsPolygonalCoupling}\left(C\right))\wedge ((\forall i\in \mathrm{Fin}\left(N\right),\forall j\in \mathrm{Fin}\left(N\right),(\neg (i=j))\Rightarrow (0<(C{)}_{i,j}))\wedge (\exists Phiout\in \mathrm{Matrix}\left(\mathrm{Fin}\left(N\right),\mathrm{Fin}\left(N\right),\mathbb{C}\right),\exists Phiin\in \mathrm{Matrix}\left(\mathrm{Fin}\left(N\right),\mathrm{Fin}\left(N\right),\mathbb{C}\right),(\mathrm{IsUnimodularDiagonal}\left(Phiout\right))\wedge ((\mathrm{IsUnimodularDiagonal}\left(Phiin\right))\wedge (((Phiout)\cdot (\mathrm{hamiltonianPropagator}\left(\mathrm{map}\left(C,\mathrm{ofReal}\right),1\right)))\cdot (Phiin)=\mathrm{fourier}\left(N\right)))))))$$

Formalization. D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.claim (✓ std3).

Citation. Edgar Barriga et al. (2026). N-dimensional discrete Fourier transform via bosonic Hamiltonian. URL: https://arxiv.org/abs/2609.05644.

Commentary.

For every positive dimension, the question asks for strictly positive off-diagonal couplings and two diagonal phase matrices whose product with the propagator at time one equals the Fourier matrix exactly.

Theorem 1.9 (Positive couplings in every dimension).

$$\forall N\in \mathbb{N},(\neg (N=0))\Rightarrow (\exists C\in \mathrm{Matrix}\left(\mathrm{Fin}\left(N\right),\mathrm{Fin}\left(N\right),\mathbb{R}\right),(\mathrm{IsPolygonalCoupling}\left(C\right))\wedge ((\forall i\in \mathrm{Fin}\left(N\right),\forall j\in \mathrm{Fin}\left(N\right),(\neg (i=j))\Rightarrow (0<(C{)}_{i,j}))\wedge (\exists Phiout\in \mathrm{Matrix}\left(\mathrm{Fin}\left(N\right),\mathrm{Fin}\left(N\right),\mathbb{C}\right),\exists Phiin\in \mathrm{Matrix}\left(\mathrm{Fin}\left(N\right),\mathrm{Fin}\left(N\right),\mathbb{C}\right),(\mathrm{IsUnimodularDiagonal}\left(Phiout\right))\wedge ((\mathrm{IsUnimodularDiagonal}\left(Phiin\right))\wedge (((Phiout)\cdot (\mathrm{hamiltonianPropagator}\left(\mathrm{map}\left(C,\mathrm{ofReal}\right),1\right)))\cdot (Phiin)=\mathrm{fourier}\left(N\right))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.result (✓ std3). ∎

Resolves. Problems/barriga-2026-polygonal-fourier-couplings (proved) by D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.result.

Source. Repository-derived.

Acknowledgement. Edgar Barriga et al. (2026). N-dimensional discrete Fourier transform via bosonic Hamiltonian. URL: https://arxiv.org/abs/2609.05644.

Commentary.

A periodic quadratic phase on the residues factors a symmetric circulant unitary as a diagonal phase, the Fourier matrix, and the same diagonal phase. Character orthogonality makes the normalized Fourier matrix unitary. Fourier conjugation diagonalizes the circulant: its eigenvalue vector is the discrete Fourier transform of its first column. The negatives of its eigenvalue arguments are real spectral angles of absolute value at most pi, and they agree at opposite residues. Their inverse Fourier kernel is therefore real and symmetric. Subtracting the mean of the angles removes the diagonal. Adding 2 pi times the quantity N minus one on the constant Fourier mode and subtracting 2 pi on every other mode preserves the exponential and raises every off-diagonal coupling by 2 pi. The original kernel has modulus at most pi, so every resulting off-diagonal coupling is strictly positive. The common phase from subtracting the mean is absorbed into the input diagonal phase.

References

• Truth anchor: D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.IsPolygonalCoupling
• Truth anchor: D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.IsUnimodularDiagonal
• Truth anchor: D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.circulant_spectral
• Truth anchor: D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.claim
• Truth anchor: D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.fourier
• Truth anchor: D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.result
• Truth anchor: D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.spectralValue
• Truth anchor: D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.transform
• Truth anchor: D5/S3/Quantum/Dynamics/PolygonalFourierCouplings.transform_unitary
• Dependency: D5/S3/Quantum/Dynamics/ProjectionProbabilityFlow
• Dependency: D5/S3/Quantum/QuantumChannels/TomiyamaDiagonalKPositivity