Exact Fourier circuits: shears

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

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

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

Each internal gate starts at an arbitrary dirty value, and its computed linear combination is added to that value. The literal zero remains literal zero.

Equations

• Complexity.ExactFourier.Program.nil.dirtyEval x✝ x_5 = Fin.snoc x✝ 0
• (p.step g).dirtyEval x✝ z = Fin.snoc (p.dirtyEval x✝ (Fin.init z)) (z (Fin.last k) + Complexity.ExactFourier.Gate.eval (p.dirtyEval x✝ (Fin.init z)) g)

theorem Complexity.ExactFourier.Gate.eval_add {w : ℕ} (g : Gate w) (v v' : Fin w → ℂ) : eval (v + v') g = eval v g + eval v' g

theorem Complexity.ExactFourier.snoc_add {n : ℕ} (v v' : Fin n → ℂ) (a a' : ℂ) : Fin.snoc (v + v') (a + a') = Fin.snoc v a + Fin.snoc v' a'

theorem Complexity.ExactFourier.Program.dirtyEval_add {n k : ℕ} (p : Program n k) (x x' : Fin n → ℂ) (z z' : Fin k → ℂ) : p.dirtyEval (x + x') (z + z') = p.dirtyEval x z + p.dirtyEval x' z'

theorem Complexity.ExactFourier.Program.dirtyEval_clean {n k : ℕ} (p : Program n k) (x : Fin n → ℂ) : p.dirtyEval x 0 = p.eval x

theorem Complexity.ExactFourier.Program.dirtyEval_split {n k : ℕ} (p : Program n k) (x : Fin n → ℂ) (z : Fin k → ℂ) : p.dirtyEval x z = p.eval x + p.dirtyEval 0 z

Exact identity behind the two replays (fft:dirty-forward, fft:dirty-output).

structure Complexity.ExactFourier.LinearDAG (n a : ℕ) : Type

A scalar circuit with independently specified input and output widths.

• size : ℕ

  The number of charged scalar gates.

• program : Program n self.size

  The scalar straight-line program containing exactly size gates.

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

  The available wire selected for each output coordinate.

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

Evaluate the program and read its designated output wires.

Equations

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

@[reducible, inline]

abbrev Complexity.ExactFourier.Shear (ι : Type u_1) : Type u_1

An elementary operation adding a scalar multiple of one coordinate to another.

Equations

• Complexity.ExactFourier.Shear ι = Matrix.TransvectionStruct ι ℂ

noncomputable def Complexity.ExactFourier.Shear.act {ι : Type u_1} (t : Shear ι) (v : ι → ℂ) : ι → ℂ

Apply one elementary shear to a vector.

Equations

• t.act v i = if i = t.i then v i + t.c * v t.j else v i

noncomputable def Complexity.ExactFourier.runShears {ι : Type u_1} (W : List (Shear ι)) (v : ι → ℂ) : ι → ℂ

Execute elementary shears from left to right on the input vector.

Equations

• Complexity.ExactFourier.runShears W v = List.foldl (fun (v : ι → ℂ) (t : Complexity.ExactFourier.Shear ι) => t.act v) v W

@[simp]

theorem Complexity.ExactFourier.runShears_nil {ι : Type u_1} (v : ι → ℂ) : runShears [] v = v

@[simp]

theorem Complexity.ExactFourier.runShears_cons {ι : Type u_1} (s : Shear ι) (W : List (Shear ι)) (v : ι → ℂ) : runShears (s :: W) v = runShears W (s.act v)

@[simp]

theorem Complexity.ExactFourier.runShears_append {ι : Type u_1} (W V : List (Shear ι)) (v : ι → ℂ) : runShears (W ++ V) v = runShears V (runShears W v)

@[simp]

theorem Complexity.ExactFourier.Shear.act_self {ι : Type u_1} (s : Shear ι) (v : ι → ℂ) : s.act v s.i = v s.i + s.c * v s.j

theorem Complexity.ExactFourier.Shear.act_other {ι : Type u_1} (s : Shear ι) (v : ι → ℂ) {a : ι} (h : a ≠ s.i) : s.act v a = v a

@[simp]

theorem Complexity.ExactFourier.Shear.act_source {ι : Type u_1} (s : Shear ι) (v : ι → ℂ) : s.act v s.j = v s.j

@[simp]

theorem Complexity.ExactFourier.Shear.inv_act_act {ι : Type u_1} (s : Shear ι) (v : ι → ℂ) : act (Matrix.TransvectionStruct.inv s) (s.act v) = v

noncomputable def Complexity.ExactFourier.reverseShears {ι : Type u_1} (W : List (Shear ι)) : List (Shear ι)

Reverse the execution order and invert every shear to undo a computation.

Equations

• Complexity.ExactFourier.reverseShears W = List.map Matrix.TransvectionStruct.inv W.reverse

@[simp]

theorem Complexity.ExactFourier.reverseShears_length {ι : Type u_1} (W : List (Shear ι)) : (reverseShears W).length = W.length

@[simp]

theorem Complexity.ExactFourier.runShears_reverse {ι : Type u_1} (W : List (Shear ι)) (v : ι → ℂ) : runShears (reverseShears W) (runShears W v) = v

def Complexity.ExactFourier.readCoord {ι : Type u_1} (r : Option ι) (v : ι → ℂ) : ℂ

none is the literal input zero, not a physical workspace coordinate.

Equations

• Complexity.ExactFourier.readCoord r v = r.elim 0 v

theorem Complexity.ExactFourier.readCoord_congr_except {ι : Type u_1} (d : ι) (r : Option ι) (h : ∀ (i : ι), r = some i → d ≠ i) (v v' : ι → ℂ) (hv : ∀ (i : ι), i ≠ d → v' i = v i) : readCoord r v' = readCoord r v

theorem Complexity.ExactFourier.add_reference {ι : Type u_1} (d : ι) (r : Option ι) (c : ℂ) (h : ∀ (i : ι), r = some i → d ≠ i) : ∃ (W : List (Shear ι)), W.length ≤ 1 ∧ ∀ (v : ι → ℂ), runShears W v d = v d + c * readCoord r v ∧ ∀ (i : ι), i ≠ d → runShears W v i = v i

Adding one permitted reference uses at most one elementary coordinate shear.

theorem Complexity.ExactFourier.add_gate {ι : Type u_1} {w : ℕ} (d : ι) (refs : Fin w → Option ι) (h : ∀ (a : Fin w) (j : ι), refs a = some j → d ≠ j) (g : Gate w) : ∃ (W : List (Shear ι)), W.length ≤ 2 ∧ ∀ (v : ι → ℂ), runShears W v d = v d + Gate.eval (fun (a : Fin w) => readCoord (refs a) v) g ∧ ∀ (i : ι), i ≠ d → runShears W v i = v i

A gate's two (or one) distinct-from-destination reads, with repeated operands allowed.

def Complexity.ExactFourier.available {n k : ℕ} (x : Fin n → ℂ) (z : Fin k → ℂ) : Fin (n + 1 + k) → ℂ

Combine the input vector, free zero, and scratch coordinates into one wire vector.

Equations

• Complexity.ExactFourier.available x z i = Fin.addCases (Fin.snoc x 0) z i

def Complexity.ExactFourier.Program.dirtyScratch {n k : ℕ} (p : Program n k) (x : Fin n → ℂ) (z : Fin k → ℂ) : Fin k → ℂ

The scratch-coordinate outputs of a program started with arbitrary scratch values.

Equations

• p.dirtyScratch x z i = p.dirtyEval x z (Fin.natAdd (n + 1) i)

theorem Complexity.ExactFourier.Program.dirtyEval_input {n k : ℕ} (p : Program n k) (x : Fin n → ℂ) (z : Fin k → ℂ) (i : Fin (n + 1)) : p.dirtyEval x z (Fin.castAdd k i) = Fin.snoc x 0 i

theorem Complexity.ExactFourier.Program.dirtyEval_available {n k : ℕ} (p : Program n k) (x : Fin n → ℂ) (z : Fin k → ℂ) : p.dirtyEval x z = available x (p.dirtyScratch x z)

@[simp]

theorem Complexity.ExactFourier.Program.dirtyScratch_step_cast {n k : ℕ} (p : Program n k) (g : Gate (n + 1 + k)) (x : Fin n → ℂ) (z : Fin (k + 1) → ℂ) (i : Fin k) : (p.step g).dirtyScratch x z i.castSucc = p.dirtyScratch x (Fin.init z) i

@[simp]

theorem Complexity.ExactFourier.Program.dirtyScratch_step_last {n k : ℕ} (p : Program n k) (g : Gate (n + 1 + k)) (x : Fin n → ℂ) (z : Fin (k + 1) → ℂ) : (p.step g).dirtyScratch x z (Fin.last k) = z (Fin.last k) + Gate.eval (p.dirtyEval x (Fin.init z)) g

def Complexity.ExactFourier.replayInputs {ι : Type u_1} {n : ℕ} (enabled : Bool) (xs : Fin n → ι) (v : ι → ℂ) : Fin n → ℂ

Read the selected input coordinates when enabled, using zeros otherwise.

Equations

• Complexity.ExactFourier.replayInputs enabled xs v i = if enabled = true then v (xs i) else 0

def Complexity.ExactFourier.referenceMap {ι : Type u_1} {n k : ℕ} (enabled : Bool) (xs : Fin n → ι) (zs : Fin k → ι) : Fin (n + 1 + k) → Option ι

Map source inputs and scratch wires to ambient coordinates, respecting the enable flag.

Equations

• Complexity.ExactFourier.referenceMap enabled xs zs i = Fin.addCases (Fin.snoc (fun (i : Fin n) => if enabled = true then some (xs i) else none) none) (fun (j : Fin k) => some (zs j)) i

theorem Complexity.ExactFourier.read_referenceMap {ι : Type u_1} {n k : ℕ} (enabled : Bool) (xs : Fin n → ι) (zs : Fin k → ι) (v : ι → ℂ) : (fun (a : Fin (n + 1 + k)) => readCoord (referenceMap enabled xs zs a) v) = available (replayInputs enabled xs v) (v ∘ zs)

theorem Complexity.ExactFourier.referenceMap_avoids {ι : Type u_1} {n k : ℕ} (enabled : Bool) (xs : Fin n → ι) (zs : Fin k → ι) (d : ι) (hx : ∀ (i : Fin n), d ≠ xs i) (hz : ∀ (j : Fin k), d ≠ zs j) (a : Fin (n + 1 + k)) (j : ι) : referenceMap enabled xs zs a = some j → d ≠ j

theorem Complexity.ExactFourier.Program.dirtySweep_exists {ι : Type u_1} {n k : ℕ} (p : Program n k) (enabled : Bool) (xs : Fin n → ι) (zs : Fin k → ι) (hz : Function.Injective zs) (hxz : ∀ (i : Fin n) (j : Fin k), xs i ≠ zs j) : ∃ (W : List (Shear ι)), W.length ≤ 2 * k ∧ ∀ (v : ι → ℂ), (∀ (j : Fin k), runShears W v (zs j) = p.dirtyScratch (replayInputs enabled xs v) (v ∘ zs) j) ∧ ∀ (r : ι), (∀ (j : Fin k), r ≠ zs j) → runShears W v r = v r

The full forward-sweep construction, with one coordinate per gate and NO zero register. Its exact semantic statement is uniform in arbitrary dirty initial values.