A tight Hessian lower bound for bilinear pairing

The polynomial sum i, x_i * y_i has a Hessian which swaps the two n-dimensional coordinate blocks. Its Hessian rank is therefore 2 * n. Since one multiplication contributes rank at most two, every arithmetic circuit over a field computing this polynomial requires at least n multiplication gates. Arbitrary additions, scalar constants, negative constants, and cancellation are allowed.

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.polynomial (K : Type) [Field K] (n : ℕ) : MvPolynomial (Fin n ⊕ Fin n) K

Bilinear pairing polynomial on two blocks of n variables.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.polynomial K n = ∑ index : Fin n, MvPolynomial.X (Sum.inl index) * MvPolynomial.X (Sum.inr index)

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.gradient_X {K : Type} [Field K] {σ : Type} [DecidableEq σ] (point : σ → K) (coordinate : σ) : gradient point (MvPolynomial.X coordinate) = Pi.single coordinate 1

The Hessian of one variable vanishes and its gradient is the corresponding coordinate vector.

def Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.swapMatrix (K : Type) [Zero K] [One K] (n : ℕ) : Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) K

Explicit block-swap matrix.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.swapMatrix K n (Sum.inl val) (Sum.inl val_1) = 0
• Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.swapMatrix K n (Sum.inl row) (Sum.inr column) = if row = column then 1 else 0
• Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.swapMatrix K n (Sum.inr row) (Sum.inl column) = if row = column then 1 else 0
• Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.swapMatrix K n (Sum.inr val) (Sum.inr val_1) = 0

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.matrix_finset_sum {K : Type} [Field K] {σ : Type} {ι : Type u_1} (point : σ → K) (indices : Finset ι) (term : ι → MvPolynomial σ K) : matrix point (∑ index ∈ indices, term index) = ∑ index ∈ indices, matrix point (term index)

Hessian formation commutes with finite sums.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.matrix_fintype_sum {K : Type} [Field K] {ι : Type u_1} {σ : Type} [Fintype ι] (point : σ → K) (term : ι → MvPolynomial σ K) : matrix point (∑ index : ι, term index) = ∑ index : ι, matrix point (term index)

Hessian formation commutes with a sum over a finite type.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.sum_matrix_apply {K : Type} [Field K] {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype ι] (term : ι → Matrix α β K) (row : α) (column : β) : (∑ index : ι, term index) row column = ∑ index : ι, term index row column

Entrywise evaluation of a finite matrix sum.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.matrix_polynomial {K : Type} [Field K] {n : ℕ} (point : Fin n ⊕ Fin n → K) : matrix point (polynomial K n) = swapMatrix K n

The pairing polynomial has the block-swap Hessian at every point.

def Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.swapLinearMap (K : Type) [Field K] (n : ℕ) : (Fin n ⊕ Fin n → K) →ₗ[K] Fin n ⊕ Fin n → K

Linear block swap induced by the Hessian.

Equations

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

@[simp]

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.swapLinearMap_self {K : Type} [Field K] {n : ℕ} (vector : Fin n ⊕ Fin n → K) : (swapLinearMap K n) ((swapLinearMap K n) vector) = vector

Swapping twice is the identity.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.swapLinearMap_surjective {K : Type} [Field K] {n : ℕ} : Function.Surjective ⇑(swapLinearMap K n)

The block-swap map is surjective.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.toLin_swapMatrix {K : Type} [Field K] {n : ℕ} : Matrix.toLin' (swapMatrix K n) = swapLinearMap K n

Matrix multiplication by the block-swap matrix performs block swap.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.linearMap_polynomial {K : Type} [Field K] {n : ℕ} (point : Fin n ⊕ Fin n → K) : linearMap point (polynomial K n) = swapLinearMap K n

The pairing Hessian endomorphism is block swap.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.rank_linearMap_polynomial {K : Type} [Field K] {n : ℕ} (point : Fin n ⊕ Fin n → K) : (linearMap point (polynomial K n)).rank = 2 * ↑n

The pairing Hessian has full rank 2 * n.

def Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.variableEquiv (n : ℕ) : Fin (2 * n) ≃ Fin n ⊕ Fin n

Enumerate the two variable blocks by the standard 2 * n circuit input type.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.variableEquiv n = (finCongr ⋯).trans finSumFinEquiv.symm

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.problem (K : Type) [Field K] (n : ℕ) : Problem (MvPolynomial (Fin n ⊕ Fin n) K)

Standard construction problem for bilinear pairing.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.circuit_multiplication_lowerBound {K : Type} [Field K] {C : Type u_1} (constant : C → K) (n : ℕ) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (constructs : (problem K n).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) : n ≤ circuit.cost Arithmetic.multiplicationCost

Bilinear pairing requires at least one multiplication per paired coordinate, over every field and with arbitrary named scalar constants.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.circuit_gate_lowerBound {K : Type} [Field K] {C : Type u_1} (constant : C → K) (n : ℕ) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (constructs : (problem K n).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) : n ≤ circuit.cost Arithmetic.gateCost

The total number of nonconstant arithmetic gates is at least n.

theorem Algebraic.Fusion.Arithmetic.Interaction.Hessian.Pairing.circuit_size_lowerBound {K : Type} [Field K] {C : Type u_1} (constant : C → K) (n : ℕ) (circuit : Circuit (Arithmetic.signature C) (2 * n) 1) (constructs : (problem K n).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) : n ≤ circuit.size

Raw circuit size is at least the pairing dimension.