CSLib representation of exact scalar Fourier circuits

Addition, subtraction, and multiplication by an arbitrary complex scalar are separate operations. All gates cost one in CSLib's gate-count model. The source's free zero wire is implemented by one additional nullary zero gate.

inductive Complexity.ExactFourier.ScalarOp : Type

The charged scalar operations, together with a constant zero gate.

• zero : ScalarOp

  Produce zero without arguments.

• add : ScalarOp

  Add two available values.

• sub : ScalarOp

  Subtract two available values.

• scale : ℂ → ScalarOp

  Multiply one available value by a fixed arbitrary complex scalar.

def Complexity.ExactFourier.scalarSignature : Cslib.Circuits.Signature

The literal scalar-operation signature, with fan-in at most two.

Equations

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

def Complexity.ExactFourier.scalarInterpretation : Cslib.Circuits.Interpretation scalarSignature ℂ

Exact complex arithmetic interprets the scalar-operation signature.

Equations

• Complexity.ExactFourier.scalarInterpretation Complexity.ExactFourier.ScalarOp.zero x_2 = 0
• Complexity.ExactFourier.scalarInterpretation Complexity.ExactFourier.ScalarOp.add x_2 = x_2 0 + x_2 1
• Complexity.ExactFourier.scalarInterpretation Complexity.ExactFourier.ScalarOp.sub x_2 = x_2 0 - x_2 1
• Complexity.ExactFourier.scalarInterpretation (Complexity.ExactFourier.ScalarOp.scale c) x_2 = c * x_2 0

def Complexity.ExactFourier.sourceWire {n k : ℕ} (i : Fin (n + 1 + k)) : Cslib.Circuits.Wire n (k + 1)

Split the source's available values into original inputs and charged CSLib gates.

Equations

• Complexity.ExactFourier.sourceWire i = if h : ↑i < n then Cslib.Circuits.Wire.input ⟨↑i, h⟩ else Cslib.Circuits.Wire.gate ⟨↑i - n, ⋯⟩

def Complexity.ExactFourier.Gate.toCslib {n k : ℕ} : Gate (n + 1 + k) → Cslib.Circuits.Line scalarSignature n (k + 1)

Translate one source operation, retaining its operands and scalar exactly.

Equations

• One or more equations did not get rendered due to their size.
• (Complexity.ExactFourier.Gate.add i j).toCslib = { op := Complexity.ExactFourier.ScalarOp.add, wires := ![Complexity.ExactFourier.sourceWire i, Complexity.ExactFourier.sourceWire j] }
• (Complexity.ExactFourier.Gate.sub i j).toCslib = { op := Complexity.ExactFourier.ScalarOp.sub, wires := ![Complexity.ExactFourier.sourceWire i, Complexity.ExactFourier.sourceWire j] }

def Complexity.ExactFourier.Program.toCslib {n k : ℕ} : Program n k → Cslib.Circuits.Program scalarSignature n (k + 1)

The zero gate followed by one CSLib gate for each source operation.

Equations

• Complexity.ExactFourier.Program.nil.toCslib = Cslib.Circuits.Program.empty.gate { op := Complexity.ExactFourier.ScalarOp.zero, wires := Fin.elim0 }
• (p.step g).toCslib = p.toCslib.gate g.toCslib

def Complexity.ExactFourier.Circuit.toCslib {n : ℕ} (C : Circuit n) : Cslib.Circuits.Circuit scalarSignature n n

Preserve designated outputs and sharing, adding only the source's free zero as a gate.

Equations

• C.toCslib = { size := C.size + 1, program := C.program.toCslib, outputs := Complexity.ExactFourier.sourceWire ∘ C.outputs }