Correctness of the scalar-circuit translation

The source's initial zero becomes gate zero. All later values retain their order, and the translation preserves every wire value and output exactly.

theorem Complexity.ExactFourier.sourceWire_castSucc {n k : ℕ} (i : Fin (n + 1 + k)) : sourceWire i.castSucc = (sourceWire i).castSucc

Old source values still denote the same wires after extending a program.

theorem Complexity.ExactFourier.sourceWire_last {n k : ℕ} : sourceWire (Fin.last (n + 1 + k)) = Cslib.Circuits.Wire.gate (Fin.last (k + 1))

The last source value is the most recently added gate.

theorem Complexity.ExactFourier.sourceWire_input {n : ℕ} (i : Fin n) : sourceWire i.castSucc = Cslib.Circuits.Wire.input i

Initial source input coordinates become input wires.

theorem Complexity.ExactFourier.sourceWire_zero (n : ℕ) : sourceWire (Fin.last n) = Cslib.Circuits.Wire.gate 0

The source's initial zero is the first gate.

theorem Complexity.ExactFourier.Gate.eval_toCslib {n k : ℕ} (g : Gate (n + 1 + k)) (x : Fin n → ℂ) (v : Fin (k + 1) → ℂ) : g.toCslib.eval scalarInterpretation x v = eval (fun (i : Fin (n + 1 + k)) => Cslib.Circuits.Wire.elim x v (sourceWire i)) g

Each translated operation uses exactly its original operands.

theorem Complexity.ExactFourier.Program.trace_toCslib {n k : ℕ} (p : Program n k) (x : Fin n → ℂ) (i : Fin (n + 1 + k)) : p.toCslib.trace scalarInterpretation x (sourceWire i) = p.eval x i

Every available source value agrees with the corresponding translated wire.

theorem Complexity.ExactFourier.Program.toCslib_fanInAtMost {n k : ℕ} (p : Program n k) : p.toCslib.FanInAtMost 2

All translated gates have at most two arguments.