A fixed polynomial envelope for the complete runtime overhead

When generated incidences and actual resources fit within a constant multiple of the source table, all overhead is at most that table size times a fixed seventh-degree polynomial in the original input length. Only the fixed geometric dimension enters the coefficient.

def Algebraic.MassProduction.Nonuniform.OverheadPolynomial.coefficient (dimension : ℕ) : ℕ

The fixed coefficient of the complete seventh-degree overhead envelope.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.OverheadPolynomial.overhead_le {inputs depth prefixWidth width suffixWidth copyBits selectorBits copies dimension : ℕ} (inputsPositive : 1 ≤ inputs) (depthSmall : depth ≤ inputs) (prefixSmall : prefixWidth ≤ inputs) (widthSmall : width ≤ inputs) (suffixSmall : suffixWidth ≤ inputs) (copySmall : copyBits ≤ inputs + 1) (selectorSmall : selectorBits ≤ inputs) (pointBudget : Sorting.networkRecords depth * 2 ^ width ≤ 2 ^ prefixWidth) (resourceBudget : HighRate.ResourceLayout.count copies dimension width ≤ 3 * 2 ^ prefixWidth) : RuntimeComposition.overhead depth copies prefixWidth dimension width suffixWidth copyBits selectorBits ≤ coefficient dimension * 2 ^ prefixWidth * inputs ^ 7

A convenient normalized parameter regime bounds every non-resource stage by coefficient dimension * 2^prefixWidth * inputs^7.