Documentation

Complexitylib.Algebraic.MassProduction.Nonuniform.FiniteBound

A fully instantiated finite high-rate mass-production bound #

The systematic code, source-bit placement, routing index widths, scheduler, and resource circuits are all constructed by proved existence theorems. Only finite numerical parameter conditions remain: positive field blocks, enough digit bits for the dimension, and the projective-direction budget.

source
def Algebraic.MassProduction.Nonuniform.FiniteBound.copies (prefixWidth dimension blockWidth blocks : ℕ) :
ℕ

Quotient-plus-one number of code copies needed by the source table.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Algebraic.MassProduction.Nonuniform.FiniteBound.costBound (depth prefixWidth dimension blockWidth blocks suffixWidth resourceBound : ℕ) :
    ℕ

    Canonically chosen routing widths and the exact finite evaluation bound.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algebraic.MassProduction.Nonuniform.FiniteBound.booleanMassComplexity_le {blockWidth blocks dimension depth prefixWidth suffixWidth resourceBound : ℕ} (blockPositive : 0 < blockWidth) (blocksPositive : 0 < blocks) (dimensionPositive : 0 < dimension) (dimensionFits : dimension ≤ 2 ^ blockWidth) (budget : 512 * Sorting.networkRecords depth * Nat.card (BinaryExtension (blockWidth * blocks)) ≤ Nat.card (Projectivization (BinaryExtension (blockWidth * blocks)) (Fin dimension → BinaryExtension (blockWidth * blocks)))) (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) (resourceBounded : ∀ (resourceFunction : ScalarFunction Bool suffixWidth), (LupanovSynthesis.lupanovCircuit suffixWidth resourceFunction).cost DeMorgan.standardCost ≤ resourceBound) :
      booleanMassComplexity (RuntimePipeline.requestFunction function) (Sorting.networkRecords depth) ≤ ↑(costBound depth prefixWidth dimension blockWidth blocks suffixWidth resourceBound)

      Complete finite mass production under numerical parameter hypotheses, using any uniform bound on the actual shorter Lupanov resource circuits.

      source
      theorem Algebraic.MassProduction.Nonuniform.FiniteBound.booleanMassComplexity_le_explicit {blockWidth blocks dimension depth prefixWidth suffixWidth : ℕ} (blockPositive : 0 < blockWidth) (blocksPositive : 0 < blocks) (dimensionPositive : 0 < dimension) (dimensionFits : dimension ≤ 2 ^ blockWidth) (budget : 512 * Sorting.networkRecords depth * Nat.card (BinaryExtension (blockWidth * blocks)) ≤ Nat.card (Projectivization (BinaryExtension (blockWidth * blocks)) (Fin dimension → BinaryExtension (blockWidth * blocks)))) (function : Fin (2 ^ prefixWidth) → (Fin suffixWidth → Bool) → Bool) :
      booleanMassComplexity (RuntimePipeline.requestFunction function) (Sorting.networkRecords depth) ≤ ↑(costBound depth prefixWidth dimension blockWidth blocks suffixWidth (LupanovRuntime.resourceCost suffixWidth))

      An unconditional finite resource envelope also gives a bound at every suffix width, before any eventual sharp-synthesis estimate is invoked.