Runtime FFT transport lemmas (NN.Runtime.*.Fft → mathlib ℂ)

NN.Runtime.Autograd.TorchLean.Fft defines FFT/IFFT matrices using “twiddle factors” written as cos θ ± i sin θ so the definitions work for TorchLean’s runtime complex scalar TorchLean.Complex β.

For the exact DFT inversion proof we instead worked in mathlib’s ℂ using primitive roots of unity (ωₙ = exp(-2πi/n)), since that is where the classical algebraic facts live.

This file bridges the two views:

• on ℂ, TorchLean’s twiddle factor is exactly ωₙ^(j*k),
• on ℂ, TorchLean’s twiddleInv factor is exactly ζₙ^(j*k),
• therefore the runtime DFT/IDFT matrices (viewed entrywise) coincide with the matrices in NN.Proofs.Analysis.Fft.

We keep the Context ℂ instance local to this module. Its ordering is arbitrary (real-part order) and is irrelevant to FFT; it exists only to instantiate the scalar-polymorphic runtime definitions at α := ℂ.

Why this is not merged into Fft.lean: Fft.lean is pure Fourier algebra over mathlib matrices. This file imports the TorchLean runtime FFT definitions and therefore sits at the boundary between runtime code and the exact theorem. The separation keeps the core inversion theorem lightweight and lets downstream proofs import only the pure DFT facts when they do not need runtime transport.

@[implicit_reducible]

def Proofs.FftBridge.instCoeNatComplex_nN : Coe ℕ ℂ

@[implicit_reducible]

def Proofs.FftBridge.instLTComplex_nN : LT ℂ

@[implicit_reducible]

def Proofs.FftBridge.instLEComplex_nN : LE ℂ

@[implicit_reducible]

noncomputable def Proofs.FftBridge.instMaxComplex_nN : Max ℂ

@[implicit_reducible]

noncomputable def Proofs.FftBridge.instMinComplex_nN : Min ℂ

@[implicit_reducible]

noncomputable def Proofs.FftBridge.instBEqComplex_nN : BEq ℂ

@[implicit_reducible]

noncomputable def Proofs.FftBridge.instMathFunctionsComplex : MathFunctions ℂ

@[implicit_reducible]

noncomputable def Proofs.FftBridge.instNumbersComplex : Numbers ℂ

@[implicit_reducible]

noncomputable def Proofs.FftBridge.instContextComplex : Context ℂ

theorem Proofs.FftBridge.twiddle_eq_omega_pow (n j k : ℕ) (hn : n ≠ 0) : Runtime.Autograd.TorchLean.NN.FFT1D.twiddle n j k = Fft.ω n ^ (j * k)

Runtime forward twiddle factors match the negative-frequency root powers from the exact DFT development.

TorchLean runtime definition:

cos θ - I * sin θ

Exact DFT definition:

ωₙ^(j*k) = exp(-2π i j k / n).

The proof is just Euler's formula plus scalar normalization of the exponent.

theorem Proofs.FftBridge.twiddleInv_eq_zeta_pow (n j k : ℕ) (hn : n ≠ 0) : Runtime.Autograd.TorchLean.NN.FFT1D.twiddleInv n j k = Fft.ζ n ^ (j * k)

Runtime inverse twiddle factors match the positive-frequency root powers from the exact IDFT development.

This is the inverse-direction analogue of twiddle_eq_omega_pow: the runtime cos θ + I * sin θ term is ζₙ^(j*k).

theorem Proofs.FftBridge.dftMatrix_entry_eq (n : ℕ) (hn : n ≠ 0) (k j : Fin n) : Spec.get2 (Runtime.Autograd.TorchLean.NN.FFT1D.dftMatrix n) k j = Fft.dftMatrix n k j

Entrywise bridge from the runtime tensor DFT matrix to the exact mathlib DFT matrix.

This is the first point where we leave pure root-of-unity algebra and connect to TorchLean's shape-indexed tensor representation.

theorem Proofs.FftBridge.idftMatrix_entry_eq (n : ℕ) (hn : n ≠ 0) (j k : Fin n) : Spec.get2 (Runtime.Autograd.TorchLean.NN.FFT1D.idftMatrix n) j k = Fft.idftMatrix n j k

Entrywise bridge from the runtime tensor IDFT matrix to the exact mathlib inverse DFT matrix.

Together with dftMatrix_entry_eq, this is the transport layer needed to reuse the pure DFT inversion theorem for runtime FFT matrix definitions.