Multiplication lower bound for bilinear pairing #
The polynomial ∑ i, xᵢ * yᵢ has a block-swap Hessian of rank 2*n. Every arithmetic circuit
computing it therefore needs at least n multiplications. This holds over every field, including
characteristic two, with arbitrary constant symbols, negative coefficients and cancellation.
Constants, additions and wiring are free. Scalar multiplications are charged.
The two variable blocks are supplied as Fin.append of the corresponding formal variables.
The premise is equality of formal polynomials, not agreement of functions over a finite field.
Main results #
Cslib.Circuits.Circuit.pairing_le_mulCost: each paired coordinate requires a multiplication.
References #
- Ported from LowerBound/Fusion/Arithmetic/Interaction/Hessian/Pairing.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.
theorem Cslib.Circuits.Circuit.pairing_le_mulCost {C : Type u_1} {K : Type u_2} [Field K] {n m : ℕ} (c : Circuit (arithSignature C) (n + n) m) (constant : C → K) (j : Fin m) (hcompute :
c.eval (arithInterpretationWith C (⇑MvPolynomial.C ∘ constant))
(Fin.append (fun (i : Fin n) => MvPolynomial.X (Sum.inl i)) fun (i : Fin n) => MvPolynomial.X (Sum.inr i)) j = ∑ i : Fin n, MvPolynomial.X (Sum.inl i) * MvPolynomial.X (Sum.inr i)) :
Computing the formal bilinear pairing requires one multiplication per paired coordinate. The conclusion bounds multiplication count, so also bounds total gate count.