Documentation

Complexitylib.Algebraic.MassProduction.LupanovParameters

Sharp Lupanov parameters #

This module selects the logarithmic address width and near-full block size for the finite Lupanov circuit. It proves the finite arithmetic estimates needed to obtain asymptotic leading coefficient one.

Uniform sharp parameters #

source
def Algebraic.MassProduction.LupanovSynthesis.lupanovAddressWidth (inputs : ℕ) :
ℕ

Three logarithmic address variables. The cap only handles the finite initial segment.

Equations
Instances For
    source
    def Algebraic.MassProduction.LupanovSynthesis.lupanovDataWidth (inputs : ℕ) :
    ℕ

    Remaining data variables.

    Equations
    Instances For
      source
      def Algebraic.MassProduction.LupanovSynthesis.lupanovBlockSize (inputs : ℕ) :
      ℕ

      Pattern block length. The lower clamp makes the finite construction well-typed for every input length and disappears asymptotically.

      Equations
      Instances For
        source
        theorem Algebraic.MassProduction.LupanovSynthesis.lupanovAddressDataSum (inputs : ℕ) :
        lupanovAddressWidth inputs + lupanovDataWidth inputs = inputs
        source
        theorem Algebraic.MassProduction.LupanovSynthesis.lupanovBlockSize_positive (inputs : ℕ) :
        0 < lupanovBlockSize inputs
        source
        theorem Algebraic.MassProduction.LupanovSynthesis.eventually_const_mul_log_le_self (constant : ℕ) :
        ∀ᶠ (inputs : ℕ) in Filter.atTop, constant * Nat.log 2 inputs ≤ inputs

        A fixed multiple of the binary logarithm is eventually below the input length.

        source
        theorem Algebraic.MassProduction.LupanovSynthesis.lupanov_parameters_eventually :
        ∀ᶠ (inputs : ℕ) in Filter.atTop, 5 * Nat.log 2 inputs < inputs ∧ lupanovAddressWidth inputs = 3 * Nat.log 2 inputs ∧ lupanovDataWidth inputs = inputs - 3 * Nat.log 2 inputs ∧ lupanovBlockSize inputs = inputs - 5 * Nat.log 2 inputs

        Finite arithmetic for the sharp estimate #

        source
        theorem Algebraic.MassProduction.LupanovSynthesis.blockCount_mul_blockSize_le (addressWidth blockSize : ℕ) (blockSizePositive : 0 < blockSize) :
        blockCount addressWidth blockSize * blockSize ≤ 2 ^ addressWidth + blockSize
        source
        theorem Algebraic.MassProduction.LupanovSynthesis.parameterCostBound_le (inputs : ℕ) (fiveLogStrict : 5 * Nat.log 2 inputs < inputs) :
        costBound (3 * Nat.log 2 inputs) (inputs - 3 * Nat.log 2 inputs) (inputs - 5 * Nat.log 2 inputs) ≤ blockCount (3 * Nat.log 2 inputs) (inputs - 5 * Nat.log 2 inputs) * 2 ^ (inputs - 3 * Nat.log 2 inputs) + 4 * inputs ^ 3 + 10 * inputs * 2 ^ (inputs - 3 * Nat.log 2 inputs)

        After selecting the classical logarithmic parameters, every term except the data-fiber term is smaller by at least three logarithmic powers.

        source
        theorem Algebraic.MassProduction.LupanovSynthesis.scaledMainTerm_le (precision inputs : ℕ) (fiveLogStrict : 5 * Nat.log 2 inputs < inputs) (removedSmall : (precision + 1) * (5 * Nat.log 2 inputs) ≤ inputs) :
        precision * inputs * (blockCount (3 * Nat.log 2 inputs) (inputs - 5 * Nat.log 2 inputs) * 2 ^ (inputs - 3 * Nat.log 2 inputs)) ≤ (precision + 1) * 2 ^ inputs + (precision + 1) * inputs * 2 ^ (inputs - 3 * Nat.log 2 inputs)

        Finite leading-term estimate. If the block length is close enough to the full input width at precision precision, the data-fiber bank contributes coefficient one plus an explicitly lower-order term.

        source
        theorem Algebraic.MassProduction.LupanovSynthesis.const_mul_square_mul_two_pow_sub_three_log_le (constant inputs : ℕ) (constantFits : 8 * constant ≤ inputs) (threeLogFits : 3 * Nat.log 2 inputs ≤ inputs) :
        constant * inputs ^ 2 * 2 ^ (inputs - 3 * Nat.log 2 inputs) ≤ 2 ^ inputs

        Three logarithmic powers absorb a fixed coefficient times n^2.