Existing DFT lower bounds apply to the imported scalar model

The scalar signature is polynomial, so the library's local linearization theorem supplies the coefficient certificate required by the DFT lower bound. The one zero gate introduced by translation is charged explicitly.

theorem Complexity.ExactFourier.scalarInterpretation_isPolynomial : Algebraic.Cutwidth.MultiOutput.Polynomial.IsPolynomial scalarInterpretation

The exact scalar operations are polynomial in their argument slots.

theorem Complexity.ExactFourier.fourierMatrix_eq_dft (n : ℕ) : fourierMatrix n = Algebraic.Cutwidth.MultiOutput.dft (zeta n) n

The source DFT matrix is the matrix used by the existing lower-bound interface.

theorem Complexity.ExactFourier.eventually_lt_cslib_size {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : Cslib.Circuits.Circuit scalarSignature n n), C.FanInAtMost 2 → C.Computes scalarInterpretation (fourierMatrix n).mulVec → (25 / 9 - ε) * ↑n < ↑C.size

All sufficiently large exact scalar Fourier circuits obey the library's linear lower bound.

theorem Complexity.ExactFourier.eventually_lt_source_size_add_one {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : Circuit n), C.Computes (fourierMatrix n) → (25 / 9 - ε) * ↑n < ↑C.size + 1

Transferring the lower bound back charges the single additional zero gate.

theorem Complexity.ExactFourier.eventually_lt_source_size {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : Circuit n), C.Computes (fourierMatrix n) → (25 / 9 - ε) * ↑n < ↑C.size

The source model itself inherits the asymptotic coefficient, absorbing the extra zero gate.