Exact Fourier circuits below every fixed multiple of n log n

OpenAI's result supplies arbitrarily large transform sizes with exact scalar circuits of size below c * n * log₂ n, for each positive c. Its equivalent minimum-size statement is a liminf of zero. The conclusion is about a cofinal set of sizes; it does not assert a uniform bound at every sufficiently large size.

The source charges each addition, subtraction, and multiplication by an arbitrary complex scalar. The CSLib translation preserves those operations and adds one zero gate. Its coefficients are unrestricted; this is not a bounded-coefficient or bit-complexity model. Source and provenance are recorded in docs/OpenAIMath.md.

The additional lower-bound corollaries use complexitylib's existing DFT results. They place the imported circuits and the library's lower bounds in one model, without a claim of new mathematical priority.

theorem Complexity.ExactFourier.minimumSize_normalized_liminf : Filter.liminf (fun (n : ℕ) => ↑(minimumSize n) / (↑n * Real.logb 2 ↑n)) Filter.atTop = 0

The literal minimum scalar gate count, normalized by n * log₂ n, has liminf zero.

theorem Complexity.ExactFourier.exists_small_fourier_circuit (c : ℝ) (hc : 0 < c) (N₀ : ℕ) : ∃ (n : ℕ), N₀ ≤ n ∧ 2 ≤ n ∧ ∃ (C : Circuit n), C.Computes (fourierMatrix n) ∧ ↑C.size < c * ↑n * Real.logb 2 ↑n

At arbitrarily large sizes, exact Fourier circuits beat any fixed n * log₂ n coefficient.

theorem Complexity.ExactFourier.exists_small_cslib_fourier_circuit (c : ℝ) (hc : 0 < c) (N₀ : ℕ) : ∃ (n : ℕ), N₀ ≤ n ∧ 2 ≤ n ∧ ∃ (C : Cslib.Circuits.Circuit scalarSignature n n), C.FanInAtMost 2 ∧ C.Computes scalarInterpretation (fourierMatrix n).mulVec ∧ ↑C.size < c * ↑n * Real.logb 2 ↑n

The same cofinal improvement holds for ordinary CSLib gate count.

theorem Complexity.ExactFourier.exists_cslib_fourier_between_bounds (ε c : ℝ) (hε : 0 < ε) (hc : 0 < c) (N₀ : ℕ) : ∃ (n : ℕ), N₀ ≤ n ∧ ∃ (C : Cslib.Circuits.Circuit scalarSignature n n), C.Computes scalarInterpretation (fourierMatrix n).mulVec ∧ (25 / 9 - ε) * ↑n < ↑C.size ∧ ↑C.size < c * ↑n * Real.logb 2 ↑n

The imported upper bounds coexist with the library's linear lower bound in one model.

theorem Complexity.ExactFourier.not_eventually_le_cslib_size (c : ℝ) (hc : 0 < c) : ¬∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : Cslib.Circuits.Circuit scalarSignature n n), C.FanInAtMost 2 → C.Computes scalarInterpretation (fourierMatrix n).mulVec → c * ↑n * Real.logb 2 ↑n ≤ ↑C.size

No positive n * log₂ n lower bound holds eventually for unrestricted scalar circuits.