Documentation

Complexitylib.Algebraic.MassProduction.UhligParameters

Parameters for Uhlig mass production #

This module chooses the logarithmic prefix width used by the sharp theorem and proves an explicit polynomial bound for the overhead of one recursive Uhlig layer.

source
def Algebraic.MassProduction.UhligTheorem.uhligPrefixWidth (inputs : ℕ) :
ℕ

We spend twice the binary logarithm of the ambient input length per two-copy layer. This makes the ordinary resource population at least the ambient input length while still costing only O(log n) variables per layer.

Equations
Instances For
    source
    def Algebraic.MassProduction.UhligTheorem.uhligBaseWidth (depth inputs : ℕ) :
    ℕ

    Inputs left for the terminal one-copy synthesis.

    Equations
    Instances For
      source
      theorem Algebraic.MassProduction.UhligTheorem.two_pow_uhligPrefixWidth_le_square (inputs : ℕ) (inputsPositive : 0 < inputs) :
      2 ^ uhligPrefixWidth inputs ≤ inputs ^ 2
      source
      theorem Algebraic.MassProduction.UhligTheorem.input_le_two_pow_uhligPrefixWidth (inputs : ℕ) (inputsLarge : 2 ≤ inputs) :
      inputs ≤ 2 ^ uhligPrefixWidth inputs
      source
      theorem Algebraic.MassProduction.UhligTheorem.uhligPrefixWidth_le_twice (inputs : ℕ) :
      uhligPrefixWidth inputs ≤ 2 * inputs
      source
      theorem Algebraic.MassProduction.UhligTheorem.layerOverheadEnvelope_eq (prefixWidth suffixWidth : ℕ) :
      UhligRecursion.layerOverheadEnvelope prefixWidth suffixWidth = have sources := 2 ^ prefixWidth; have resources := sources + 1; resources * (suffixWidth * (2 * sources * resources * (prefixWidth + 1))) + 2 * (sources * (sources * (4 * prefixWidth + 4 * resources + 2) + sources) + sources)

      Expanded polynomial for the cost of one pair-factored Uhlig layer.

      source
      theorem Algebraic.MassProduction.UhligTheorem.layerOverheadEnvelope_uhligPrefixWidth_le (inputs : ℕ) (inputsLarge : 2 ≤ inputs) :
      UhligRecursion.layerOverheadEnvelope (uhligPrefixWidth inputs) inputs ≤ 64 * inputs ^ 8

      With the chosen logarithmic prefix, the entire pair-factored layer overhead is bounded by a fixed degree-eight monomial.