Polynomial-degree fusion lower bounds

Polynomial natDegree is a dyadic arithmetic measure: addition is bounded by the maximum of the input degrees, multiplication by their sum, and scalar constants have degree zero. The generic dyadic fusion theorem therefore gives a multiplicative-complexity lower bound from the degree of the target.

As a concrete exact-scale example, constructing X ^ (2 ^ n) from X and arbitrary scalar constants requires at least n multiplication gates. The statement permits an unrestricted number of free additions.

def Algebraic.Fusion.PolynomialDegree.measure (K : Type u) [Semiring K] : Dyadic.Measure K (Polynomial K) ⇑Polynomial.C

Polynomial natural degree as a degree-like dyadic measure.

Equations

• Algebraic.Fusion.PolynomialDegree.measure K = { value := Polynomial.natDegree, add_le := ⋯, mul_le := ⋯, constant_le_one := ⋯ }

theorem Algebraic.Fusion.PolynomialDegree.multiplication_lowerBound {K : Type u} [Semiring K] (problem : Problem (Polynomial K)) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), (problem.inputs input).natDegree ≤ 1) (target_ge : 2 ^ levels ≤ problem.target.natDegree) (circuit : Circuit (Arithmetic.signature K) problem.inputCount 1) (constructs : problem.Constructs circuit (Arithmetic.interpretation ⇑Polynomial.C)) : levels ≤ circuit.cost Arithmetic.multiplicationCost

Polynomial degree gives a multiplication lower bound for any construction problem whose generators have degree at most one.

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.PolynomialDegree.powerProblem (K : Type u) [Semiring K] (n : ℕ) : Problem (Polynomial K)

Construct the power X ^ (2 ^ n) from the single generator X.

Equations

• Algebraic.Fusion.PolynomialDegree.powerProblem K n = { inputCount := 1, inputs := fun (x : Fin 1) => Polynomial.X, target := Polynomial.X ^ 2 ^ n }

theorem Algebraic.Fusion.PolynomialDegree.power_multiplication_lowerBound {n : ℕ} {K : Type u} [Semiring K] [Nontrivial K] (circuit : Circuit (Arithmetic.signature K) 1 1) (constructs : (powerProblem K n).Constructs circuit (Arithmetic.interpretation ⇑Polynomial.C)) : n ≤ circuit.cost Arithmetic.multiplicationCost

Computing X ^ (2 ^ n) requires at least n multiplications, even with arbitrary scalar constants and free additions.