Complex Multiplication: Correctness and Cost Analysis

A simple example showing how to use FreeM.cost with variable/parametrized query costs.

We prove that both complexMulNaive and complexMulGauss correctly compute complex multiplication when given an honest oracle, and compute their exact costs under a parametric weight function. The cost theorems hold for any oracle (not just honest ones), because both algorithms are straight-line (no branching on query results).

Correctness

theorem Cslib.Query.complexMulNaive_eval_honest {α : Type} [Add α] [Sub α] [Mul α] (a b c d : α) : FreeM.eval (fun {ι : Type} => ArithQuery.honest) (complexMulNaive a b c d) = (a * c - b * d, a * d + b * c)

theorem Cslib.Query.complexMulGauss_eval_honest {α : Type} [CommRing α] (a b c d : α) : FreeM.eval (fun {ι : Type} => ArithQuery.honest) (complexMulGauss a b c d) = (a * c - b * d, a * d + b * c)

Exact cost counts

theorem Cslib.Query.complexMulNaive_cost {α : Type} (oracle : {ι : Type} → ArithQuery α ι → ι) (c_add c_mul : ℕ) (a b c d : α) : FreeM.cost (fun {ι : Type} => oracle) (fun {ι : Type} => ArithQuery.weight c_add c_mul) (complexMulNaive a b c d) = 4 * c_mul + 2 * c_add

theorem Cslib.Query.complexMulGauss_cost {α : Type} (oracle : {ι : Type} → ArithQuery α ι → ι) (c_add c_mul : ℕ) (a b c d : α) : FreeM.cost (fun {ι : Type} => oracle) (fun {ι : Type} => ArithQuery.weight c_add c_mul) (complexMulGauss a b c d) = 3 * c_mul + 5 * c_add

Crossover: Gauss beats naive when multiplication costs at least 3× addition

theorem Cslib.Query.gauss_le_naive {α : Type} (oracle : {ι : Type} → ArithQuery α ι → ι) (c_add c_mul : ℕ) (a b c d : α) (h : 3 * c_add ≤ c_mul) : FreeM.cost (fun {ι : Type} => oracle) (fun {ι : Type} => ArithQuery.weight c_add c_mul) (complexMulGauss a b c d) ≤ FreeM.cost (fun {ι : Type} => oracle) (fun {ι : Type} => ArithQuery.weight c_add c_mul) (complexMulNaive a b c d)

theorem Cslib.Query.gauss_le_naive_iff {α : Type} (oracle : {ι : Type} → ArithQuery α ι → ι) (c_add c_mul : ℕ) (a b c d : α) : FreeM.cost (fun {ι : Type} => oracle) (fun {ι : Type} => ArithQuery.weight c_add c_mul) (complexMulGauss a b c d) ≤ FreeM.cost (fun {ι : Type} => oracle) (fun {ι : Type} => ArithQuery.weight c_add c_mul) (complexMulNaive a b c d) ↔ 3 * c_add ≤ c_mul