A near-linear bound for the complete nonuniform scheduler

The exact recursive cost sum is bounded by total * 2^width times an explicit fixed polynomial in the address width, request width, field width, and ceiling logarithm of the original request count.

def Algebraic.MassProduction.Nonuniform.BufferIteration.polynomialFactor (total dimension width requestWidth : ℕ) : ℕ

Polynomial overhead per original request and field scalar.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.BufferIteration.costBound_le_phaseCount {completed requestDepth total dimension width requestWidth : ℕ} (counts : completed + Sorting.networkRecords requestDepth = total) : costBound total dimension width requestWidth requestDepth completed ≤ (requestDepth + 1) * (10000 * (total * 2 ^ width * (14 + 18 * (dimension * width))) * BufferedPhase.height total dimension width requestWidth ^ 5)

Sum at most one uniform phase bound for every halving depth.

theorem Algebraic.MassProduction.Nonuniform.BufferIteration.costBound_le_linear {completed requestDepth total dimension width requestWidth : ℕ} (counts : completed + Sorting.networkRecords requestDepth = total) : costBound total dimension width requestWidth requestDepth completed ≤ total * 2 ^ width * polynomialFactor total dimension width requestWidth

The complete phase sum is linear in the original point budget.

theorem Algebraic.MassProduction.Nonuniform.BufferIteration.existsCircuit_linear {width dimension completed requestDepth total requestWidth : ℕ} (positive : 0 < width) (dimensionPositive : 0 < dimension) (counts : completed + Sorting.networkRecords requestDepth = total) (budget : 512 * total * Nat.card (BinaryExtension width) ≤ Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (targetProjection : Fin (dimension * width) → Fin requestWidth) : ∃ (scheduler : Circuit DeMorgan.signature (BufferInput.inputWidth completed (Sorting.networkRecords requestDepth) requestWidth (2 ^ width) (dimension * width)) (BufferInput.inputWidth total 0 requestWidth (2 ^ width) (dimension * width))), scheduler.cost DeMorgan.standardCost ≤ total * 2 ^ width * polynomialFactor total dimension width requestWidth ∧ BufferModel.Transforms positive targetProjection scheduler total

One fixed, near-linear-size circuit completes every valid input buffer under the projective-direction budget.