Documentation

Complexitylib.Algebraic.MassProduction.Nonuniform.BufferedPhaseCost

Uniform cost bounds over the buffer phases #

All phase depths are bounded using the logarithm of the original request count. The resulting bound is linear in total * 2^width; all remaining factors are polynomial in bit widths and logarithms.

source
def Algebraic.MassProduction.Nonuniform.BufferedPhase.height (total dimension width requestWidth : ℕ) :
ℕ

A uniform bound on the polynomial parameters of every phase.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algebraic.MassProduction.Nonuniform.BufferedPhase.requestDepth_le {requestDepth total : ℕ} (activeLe : Sorting.networkRecords requestDepth ≤ total) :
    requestDepth ≤ FiniteParameters.binaryDepth total

    Every active sorting depth is at most the original batch's ceiling logarithm.

    source
    theorem Algebraic.MassProduction.Nonuniform.BufferedPhase.menuDepth_le {requestDepth total dimension width : ℕ} (activeLe : Sorting.networkRecords requestDepth ≤ total) :
    menuDepth total requestDepth dimension width ≤ FiniteParameters.binaryDepth total + dimension * width + 2

    The menu depth adds at most the geometric address width and two bits.

    source
    theorem Algebraic.MassProduction.Nonuniform.BufferedPhase.routingDepth_le {completed total requestDepth dimension width : ℕ} (completedLe : completed ≤ total) (activeLe : Sorting.networkRecords requestDepth ≤ total) :
    routingDepth total completed requestDepth dimension width ≤ 2 * FiniteParameters.binaryDepth total + dimension * width + width + 3

    Canonical occupancy routing has logarithmic depth in the original point budget.

    source
    theorem Algebraic.MassProduction.Nonuniform.BufferedPhase.pointCount_le {requestDepth total dimension width : ℕ} (activeLe : Sorting.networkRecords requestDepth ≤ total) :
    Sorting.networkRecords (menuDepth total requestDepth dimension width + requestDepth + width) ≤ 2 * (total * (2 + 3 * (dimension * width))) * 2 ^ width

    Every generated point array is linear in the original number of requests.

    source
    theorem Algebraic.MassProduction.Nonuniform.BufferedPhase.pointAndRoutingCount_le {completed total requestDepth dimension width : ℕ} (completedLe : completed ≤ total) (activeLe : Sorting.networkRecords requestDepth ≤ total) :
    Sorting.networkRecords (menuDepth total requestDepth dimension width + requestDepth + width) + Sorting.networkRecords (routingDepth total completed requestDepth dimension width) ≤ total * 2 ^ width * (14 + 18 * (dimension * width))

    The combined generated and padded occupancy arrays remain linear.

    source
    theorem Algebraic.MassProduction.Nonuniform.BufferedPhase.costBound_le {completed total requestDepth dimension width requestWidth : ℕ} (completedLe : completed ≤ total) (activeLe : Sorting.networkRecords requestDepth ≤ total) :
    costBound total completed requestDepth dimension width requestWidth ≤ 10000 * (total * 2 ^ width * (14 + 18 * (dimension * width))) * height total dimension width requestWidth ^ 5

    One compacted phase has a cost linear in the original point budget, with a fixed polynomial factor independent of the active request count.