Circulants and odd cosine pairing

Abstract

Fourier modes factor circulant characteristic polynomials.

Theorem 1.1 (Fourier transform determinant).

$$\forall (n:\mathbb{N}),([\mathrm{NeZero}\left(n\right)]Matrix.det\left(D5.S3.Quantum.Dynamics.PolygonalFourierCouplings.transform\left(n\right)\right)\ne (0:\mathbb{C}))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CirculantCharpoly.transform_det_ne_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The normalized Fourier matrix has nonzero determinant because its conjugate transpose is an inverse.

Theorem 1.2 (Complex circulant factorization).

Lean statement: D5/S3/Quantum/Matrix/CirculantCharpoly.circulant_charpoly

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CirculantCharpoly.circulant_charpoly (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Tanvi Jain (2017). Hadamard powers of some positive matrices. DOI: 10.1016/j.laa.2016.06.030. URL: https://doi.org/10.1016/j.laa.2016.06.030.

Commentary.

The characteristic polynomial of a complex circulant is the product of X minus its discrete Fourier values. This theorem is existing repository content reused from the Roldan circulant energy development.

Theorem 1.3 (Reality of even Fourier values).

Lean statement: D5/S3/Quantum/Matrix/CirculantCharpoly.dft_real_of_even

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CirculantCharpoly.dft_real_of_even (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Tanvi Jain (2017). Hadamard powers of some positive matrices. DOI: 10.1016/j.laa.2016.06.030. URL: https://doi.org/10.1016/j.laa.2016.06.030.

Commentary.

The discrete Fourier value of an even real function is real. This theorem is existing repository content reused from the Roldan circulant energy development.

Theorem 1.4 (Real circulant factorization).

Lean statement: D5/S3/Quantum/Matrix/CirculantCharpoly.real_circulant_charpoly

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CirculantCharpoly.real_circulant_charpoly (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Tanvi Jain (2017). Hadamard powers of some positive matrices. DOI: 10.1016/j.laa.2016.06.030. URL: https://doi.org/10.1016/j.laa.2016.06.030.

Commentary.

An even real circulant has the product of X minus the real parts of its Fourier values. This theorem is existing repository content reused from the Roldan circulant energy development.

Definition 1.5 (Real residue entries).

Lean statement: D5/S3/Quantum/Matrix/CirculantCharpoly.realCirculant

Formalization. D5/S3/Quantum/Matrix/CirculantCharpoly.realCirculant (✓ std3).

Source. Repository-derived.

Acknowledgement. Tanvi Jain (2017). Hadamard powers of some positive matrices. DOI: 10.1016/j.laa.2016.06.030. URL: https://doi.org/10.1016/j.laa.2016.06.030.

Commentary.

For order 2m+1, the circulant entry is f at the least nonnegative residue.

Definition 1.6 (Cosine mode values).

Lean statement: D5/S3/Quantum/Matrix/CirculantCharpoly.cosineValue

Formalization. D5/S3/Quantum/Matrix/CirculantCharpoly.cosineValue (✓ std3).

Source. Repository-derived.

Acknowledgement. Tanvi Jain (2017). Hadamard powers of some positive matrices. DOI: 10.1016/j.laa.2016.06.030. URL: https://doi.org/10.1016/j.laa.2016.06.030.

Commentary.

The real mode is f(0) plus twice the cosine sum from one through m.

Theorem 1.7 (Opposite character values).

$$\forall (n:\mathbb{N}),([\mathrm{NeZero}\left(n\right)]\forall (j:\mathbb{N}),(\forall (l:\mathbb{N}),((l\le n)\Rightarrow (ZMod.stdAddChar\left(((j:\mathrm{ZMod}\left(n\right)))\cdot ((l:\mathrm{ZMod}\left(n\right)))\right)+ZMod.stdAddChar\left(((j:\mathrm{ZMod}\left(n\right)))\cdot (((n-l:\mathbb{N}):\mathrm{ZMod}\left(n\right)))\right)=((((2:\mathbb{R}))\cdot (Real.cos\left(\frac{((((2:\mathbb{R}))\cdot (Real.pi))\cdot ((j:\mathbb{R})))\cdot ((l:\mathbb{R}))}{(n:\mathbb{R})}\right)):\mathbb{R}):\mathbb{C})))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CirculantCharpoly.character_pair (✓ std3). ∎

Source. Repository-derived.

Commentary.

For the standard complex additive character on ZMod n, opposite residues pair to twice the cosine of their angle; natural arguments are cast into ZMod n and the real right side is cast into the complex numbers.

Theorem 1.8 (Odd paired factorization).

Lean statement: D5/S3/Quantum/Matrix/CirculantCharpoly.realCirculant_charpoly

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/CirculantCharpoly.realCirculant_charpoly (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Tanvi Jain (2017). Hadamard powers of some positive matrices. DOI: 10.1016/j.laa.2016.06.030. URL: https://doi.org/10.1016/j.laa.2016.06.030.

Commentary.

For an even generating function, the odd real characteristic polynomial has one constant factor and squared factors for modes one through m. Pairing opposite residues gives the cosine formula and pairing opposite modes gives the squares. This odd pairing factorization is proved here.

References

• Truth anchor: D5/S3/Quantum/Matrix/CirculantCharpoly.character_pair
• Truth anchor: D5/S3/Quantum/Matrix/CirculantCharpoly.circulant_charpoly
• Truth anchor: D5/S3/Quantum/Matrix/CirculantCharpoly.cosineValue
• Truth anchor: D5/S3/Quantum/Matrix/CirculantCharpoly.dft_real_of_even
• Truth anchor: D5/S3/Quantum/Matrix/CirculantCharpoly.realCirculant
• Truth anchor: D5/S3/Quantum/Matrix/CirculantCharpoly.realCirculant_charpoly
• Truth anchor: D5/S3/Quantum/Matrix/CirculantCharpoly.real_circulant_charpoly
• Truth anchor: D5/S3/Quantum/Matrix/CirculantCharpoly.transform_det_ne_zero
• Dependency: D5/S3/Quantum/Dynamics/PolygonalFourierCouplings