Exact Fourier circuits: core

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/Core.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

inductive Complexity.ExactFourier.Gate (w : ℕ) : Type

One charged scalar gate, referencing only available values.

• add {w : ℕ} (i j : Fin w) : Gate w

  One charged addition.

• sub {w : ℕ} (i j : Fin w) : Gate w

  One charged subtraction.

• scale {w : ℕ} (c : ℂ) (i : Fin w) : Gate w

  One charged multiplication by an arbitrary complex scalar.

def Complexity.ExactFourier.Gate.eval {w : ℕ} (v : Fin w → ℂ) : Gate w → ℂ

Evaluate a scalar gate on the currently available values.

Equations

• Complexity.ExactFourier.Gate.eval v (Complexity.ExactFourier.Gate.add i j) = v i + v j
• Complexity.ExactFourier.Gate.eval v (Complexity.ExactFourier.Gate.sub i j) = v i - v j
• Complexity.ExactFourier.Gate.eval v (Complexity.ExactFourier.Gate.scale c i) = c * v i

inductive Complexity.ExactFourier.Program (n : ℕ) : ℕ → Type

A topologically ordered scalar DAG; available values are never consumed.

• nil {n : ℕ} : Program n 0

  Initial inputs and a free zero wire.

• step {n k : ℕ} (p : Program n k) (g : Gate (n + 1 + k)) : Program n (k + 1)

  Append one operation whose operands are already available.

def Complexity.ExactFourier.Program.eval {n k : ℕ} : Program n k → (Fin n → ℂ) → Fin (n + 1 + k) → ℂ

All available values, with inputs first, then zero, then computed gate values.

Equations

• Complexity.ExactFourier.Program.nil.eval x✝ = Fin.snoc x✝ 0
• (p.step g).eval x✝ = Fin.snoc (p.eval x✝) (Complexity.ExactFourier.Gate.eval (p.eval x✝) g)

structure Complexity.ExactFourier.Circuit (n : ℕ) : Type

Outputs name available values, so permutations and arbitrary fanout are uncharged.

• size : ℕ

  The number of charged scalar operations.

• program : Program n self.size

  The topologically ordered operations.

• outputs : Fin n → Fin (n + 1 + self.size)

  A freely chosen available wire for each output coordinate.

def Complexity.ExactFourier.Circuit.eval {n : ℕ} (C : Circuit n) (x : Fin n → ℂ) : Fin n → ℂ

Read all designated outputs after evaluating the program.

Equations

• C.eval x i = C.program.eval x (C.outputs i)

noncomputable def Complexity.ExactFourier.zeta (n : ℕ) : ℂ

The standard complex root used by the exact discrete Fourier transform.

Equations

• Complexity.ExactFourier.zeta n = Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)

noncomputable def Complexity.ExactFourier.fourierMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℂ

The unnormalized DFT matrix, with positive exponential sign.

Equations

• Complexity.ExactFourier.fourierMatrix n j k = Complexity.ExactFourier.zeta n ^ (↑j * ↑k)

def Complexity.ExactFourier.Circuit.Computes {n : ℕ} (C : Circuit n) (A : Matrix (Fin n) (Fin n) ℂ) : Prop

Exact matrix multiplication on every complex input vector.

Equations

• C.Computes A = ∀ (x : Fin n → ℂ), C.eval x = A.mulVec x

def Complexity.ExactFourier.MainStatement : Prop

Arbitrarily large sizes admit circuits below any fixed multiple of n * log₂ n.

Equations

• One or more equations did not get rendered due to their size.