The complete fixed halving iteration

Compose one universal compacted phase for each pending power of two, ending with the singleton phase. The circuit completes every original request and preserves the disjoint-schedule invariant. Its cost is bounded by the exact recursive sum of the explicit phase bounds.

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

Sum of the explicit phase bounds along the fixed halving schedule.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.BufferIteration.existsCircuit {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 (completed + Sorting.networkRecords requestDepth) 0 requestWidth (2 ^ width) (dimension * width))), scheduler.cost DeMorgan.standardCost ≤ costBound total dimension width requestWidth requestDepth completed ∧ BufferModel.Transforms positive targetProjection scheduler total

One concrete circuit completes all halving phases and leaves no pending requests, preserving the full encoded request and geometric invariants.

theorem Algebraic.MassProduction.Nonuniform.BufferIteration.existsCircuit_complete {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 ≤ costBound total dimension width requestWidth requestDepth completed ∧ BufferModel.Transforms positive targetProjection scheduler total

The completed-count equality may be used to expose an output buffer indexed by the original total request count.