Exact Fourier circuits: linear dag

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

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

def Complexity.ExactFourier.Gate.map {w w' : ℕ} (f : Fin w → Fin w') : Gate w → Gate w'

Relabel every input wire of a scalar gate.

Equations

• Complexity.ExactFourier.Gate.map f (Complexity.ExactFourier.Gate.add i j) = Complexity.ExactFourier.Gate.add (f i) (f j)
• Complexity.ExactFourier.Gate.map f (Complexity.ExactFourier.Gate.sub i j) = Complexity.ExactFourier.Gate.sub (f i) (f j)
• Complexity.ExactFourier.Gate.map f (Complexity.ExactFourier.Gate.scale c i) = Complexity.ExactFourier.Gate.scale c (f i)

theorem Complexity.ExactFourier.Gate.eval_map {w w' : ℕ} (f : Fin w → Fin w') (g : Gate w) (v : Fin w' → ℂ) : eval v (map f g) = eval (v ∘ f) g

def Complexity.ExactFourier.appendIndex {n m k l : ℕ} (f : Fin (m + 1) → Fin (n + 1 + k)) (i : Fin (m + 1 + l)) : Fin (n + 1 + (k + l))

Relocate a wire when appending a program to an existing computation.

Equations

• Complexity.ExactFourier.appendIndex f i = if h : ↑i < m + 1 then ⟨↑(f ⟨↑i, h⟩), ⋯⟩ else ⟨n + 1 + k + (↑i - (m + 1)), ⋯⟩

def Complexity.ExactFourier.keepIndex {n k l : ℕ} (i : Fin (n + 1 + k)) : Fin (n + 1 + (k + l))

Retain an existing wire index after appending more gates.

Equations

• Complexity.ExactFourier.keepIndex i = ⟨↑i, ⋯⟩

@[simp]

theorem Complexity.ExactFourier.appendIndex_last {n m k l : ℕ} (f : Fin (m + 1) → Fin (n + 1 + k)) : appendIndex f (Fin.last (m + 1 + l)) = Fin.last (n + 1 + (k + l))

@[simp]

theorem Complexity.ExactFourier.appendIndex_castSucc {n m k l : ℕ} (f : Fin (m + 1) → Fin (n + 1 + k)) (i : Fin (m + 1 + l)) : appendIndex f i.castSucc = (appendIndex f i).castSucc

@[simp]

theorem Complexity.ExactFourier.keepIndex_succ {n k l : ℕ} (i : Fin (n + 1 + k)) : keepIndex i = (keepIndex i).castSucc

@[simp]

theorem Complexity.ExactFourier.keepIndex_zero {n k : ℕ} (i : Fin (n + 1 + k)) : keepIndex i = i

@[simp]

theorem Complexity.ExactFourier.appendIndex_zero {n m k : ℕ} (f : Fin (m + 1) → Fin (n + 1 + k)) (i : Fin (m + 1)) : appendIndex f i = f i

def Complexity.ExactFourier.Program.append {n m k : ℕ} (p : Program n k) (f : Fin (m + 1) → Fin (n + 1 + k)) {l : ℕ} : Program m l → Program n (k + l)

Append a scalar program using the supplied references for its inputs and zero wire.

Equations

• p.append f Complexity.ExactFourier.Program.nil = p
• p.append f (q.step g) = (p.append f q).step (Complexity.ExactFourier.Gate.map (Complexity.ExactFourier.appendIndex f) g)

theorem Complexity.ExactFourier.Program.eval_append {n m k l : ℕ} (p : Program n k) (q : Program m l) (f : Fin (m + 1) → Fin (n + 1 + k)) (x : Fin n → ℂ) (y : Fin m → ℂ) (hf : ∀ (i : Fin (m + 1)), p.eval x (f i) = Fin.snoc y 0 i) : (∀ (j : Fin (n + 1 + k)), (p.append f q).eval x (keepIndex j) = p.eval x j) ∧ ∀ (i : Fin (m + 1 + l)), (p.append f q).eval x (appendIndex f i) = q.eval y i

Literal semantics of DAG composition, including preservation of every existing value.

noncomputable def Complexity.ExactFourier.LinearDAG.comp {n a b : ℕ} (D : LinearDAG a b) (C : LinearDAG n a) : LinearDAG n b

Exact composition: all previous values can be reused without being consumed.

Equations

• D.comp C = { size := C.size + D.size, program := C.program.append (Fin.snoc C.outputs ⟨n, ⋯⟩) D.program, outputs := Complexity.ExactFourier.appendIndex (Fin.snoc C.outputs ⟨n, ⋯⟩) ∘ D.outputs }

theorem Complexity.ExactFourier.Program.eval_zero {n k : ℕ} (p : Program n k) (x : Fin n → ℂ) : p.eval x ⟨n, ⋯⟩ = 0

theorem Complexity.ExactFourier.Program.eval_input {n k : ℕ} (p : Program n k) (x : Fin n → ℂ) (j : Fin n) : p.eval x ⟨↑j, ⋯⟩ = x j

theorem Complexity.ExactFourier.LinearDAG.eval_comp {n a b : ℕ} (D : LinearDAG a b) (C : LinearDAG n a) (x : Fin n → ℂ) : (D.comp C).eval x = D.eval (C.eval x)

def Complexity.ExactFourier.gateIndex {n k a : ℕ} (i : Fin a) : Fin (n + 1 + (k + a))

Index of a newly emitted vector gate.

Equations

• Complexity.ExactFourier.gateIndex i = ⟨n + 1 + k + ↑i, ⋯⟩

@[simp]

theorem Complexity.ExactFourier.gateIndex_last {n k a : ℕ} : gateIndex (Fin.last a) = Fin.last (n + 1 + (k + a))

@[simp]

theorem Complexity.ExactFourier.gateIndex_castSucc {n k a : ℕ} (i : Fin a) : gateIndex i.castSucc = (gateIndex i).castSucc

def Complexity.ExactFourier.Program.emit {n k : ℕ} (p : Program n k) {a : ℕ} : (Fin a → Gate (n + 1 + k)) → Program n (k + a)

Emit independent scalar operations, one cost unit per coordinate, with original operands still available after the whole layer.

Equations

• p.emit x_2 = p
• p.emit g = (p.emit (g ∘ Fin.castSucc)).step (Complexity.ExactFourier.Gate.map Complexity.ExactFourier.keepIndex (g (Fin.last a)))

theorem Complexity.ExactFourier.Program.eval_emit {n k a : ℕ} (p : Program n k) (g : Fin a → Gate (n + 1 + k)) (x : Fin n → ℂ) : (∀ (j : Fin (n + 1 + k)), (p.emit g).eval x (keepIndex j) = p.eval x j) ∧ ∀ (i : Fin a), (p.emit g).eval x (gateIndex i) = Gate.eval (p.eval x) (g i)

def Complexity.ExactFourier.LinearDAG.wires {n a : ℕ} (f : Fin a → Fin (n + 1)) : LinearDAG n a

Read-only input relabeling and arbitrary fanout are genuinely free.

Equations

• Complexity.ExactFourier.LinearDAG.wires f = { size := 0, program := Complexity.ExactFourier.Program.nil, outputs := f }

@[simp]

theorem Complexity.ExactFourier.LinearDAG.eval_wires {n a : ℕ} (f : Fin a → Fin (n + 1)) (x : Fin n → ℂ) : (wires f).eval x = fun (i : Fin a) => Fin.snoc x 0 (f i)

def Complexity.ExactFourier.LinearDAG.layer {n a : ℕ} (g : Fin a → Gate (n + 1)) : LinearDAG n a

A rectangular vector layer still charges every scalar gate separately.

Equations

• Complexity.ExactFourier.LinearDAG.layer g = { size := 0 + a, program := Complexity.ExactFourier.Program.nil.emit g, outputs := Complexity.ExactFourier.gateIndex }

@[simp]

theorem Complexity.ExactFourier.LinearDAG.size_layer {n a : ℕ} (g : Fin a → Gate (n + 1)) : (layer g).size = a

theorem Complexity.ExactFourier.LinearDAG.eval_layer {n a : ℕ} (g : Fin a → Gate (n + 1)) (x : Fin n → ℂ) : (layer g).eval x = fun (i : Fin a) => Gate.eval (Fin.snoc x 0) (g i)

def Complexity.ExactFourier.LinearDAG.addColumn {n a : ℕ} (C : LinearDAG n a) (j : Fin n) (c : Fin a → ℂ) : LinearDAG n a

Append a scaled original input into each existing output accumulator. The two scalar operations per row are charged even for a zero scalar.

Equations

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

theorem Complexity.ExactFourier.LinearDAG.eval_addColumn {n a : ℕ} (C : LinearDAG n a) (j : Fin n) (c : Fin a → ℂ) (x : Fin n → ℂ) : (C.addColumn j c).eval x = fun (i : Fin a) => C.eval x i + c i * x j

def Complexity.ExactFourier.LinearDAG.matrix (n a : ℕ) (G : Matrix (Fin a) (Fin n) ℂ) : LinearDAG n a

Direct multiplication: this construction will be used only for the fixed spatial matrices in the coefficient-boundary comparison, not as a purported FFT saving.

Equations

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

@[simp]

theorem Complexity.ExactFourier.LinearDAG.size_matrix {n a : ℕ} (G : Matrix (Fin a) (Fin n) ℂ) : (matrix n a G).size = 2 * a * n

theorem Complexity.ExactFourier.LinearDAG.eval_matrix {n a : ℕ} (G : Matrix (Fin a) (Fin n) ℂ) (x : Fin n → ℂ) : (matrix n a G).eval x = G.mulVec x

theorem Complexity.ExactFourier.MatrixPrice.twoWay_DAG_bound (p : MatrixPrice) {n : ℕ} (G : Matrix (Fin n) (Fin n) ℂ) (hG : IsUnit G) (C D : LinearDAG n n) (hC : ∀ (x : Fin n → ℂ), C.eval x = G.mulVec x) (hD : ∀ (x : Fin n → ℂ), D.eval x = G⁻¹.mulVec x) : p.value G ≤ 8 * ↑C.size + 4 * ↑D.size + 3 * ↑n

Quantitative version of the two-way pre-corner argument, with no hidden inverse oracle: D is an actual charged DAG computing the inverse map.

theorem Complexity.ExactFourier.MatrixPrice.quadratic_bound (p : MatrixPrice) {n : ℕ} (G : Matrix (Fin n) (Fin n) ℂ) (hG : IsUnit G) : p.value G ≤ 24 * ↑n ^ 2 + 3 * ↑n

Uniform finite upper bound needed in the compactness branch. It does not assert that any price exists; it is a consequence of the standing price laws.