Exact scalar circuits transfer to CSLib

The translation preserves every output and all sharing. It adds exactly one gate, for the source's free zero wire. Every addition, subtraction, and scalar multiplication remains a separate gate of fan-in at most two.

theorem Complexity.ExactFourier.Circuit.size_toCslib {n : ℕ} (C : Circuit n) : C.toCslib.size = C.size + 1

The only additional gate produces the source's free zero wire.

theorem Complexity.ExactFourier.Circuit.eval_toCslib {n : ℕ} (C : Circuit n) (x : Fin n → ℂ) : C.toCslib.eval scalarInterpretation x = C.eval x

The translation preserves the complete vector of outputs.

theorem Complexity.ExactFourier.Circuit.Computes.toCslib {n : ℕ} {C : Circuit n} {A : Matrix (Fin n) (Fin n) ℂ} (hC : C.Computes A) : C.toCslib.Computes scalarInterpretation A.mulVec

Source matrix computation becomes literal CSLib function computation.

theorem Complexity.ExactFourier.Circuit.toCslib_fanInAtMost {n : ℕ} (C : Circuit n) : C.toCslib.FanInAtMost 2

Source scalar circuits translate to CSLib circuits of fan-in at most two.