Unrolled greedy scheduler circuits

This module unrolls the manuscript's greedy scheduler over a fixed request group. The state retains all previously emitted punctured-line points and the next stage pads its power-of-two sorting array with the current target; those padding positions generate zero differences and hence sentinel ranks.

No new global field or finite-enumeration instances are introduced. The request count, sorter depth, and slot-capacity proof are ordinary parameters of the nonuniform circuit family.

@[reducible]

def Algebraic.MassProduction.SchedulerIteration.pointBitWidth (dimension width : ℕ) : ℕ

Packed width of one affine-space point.

Equations

• Algebraic.MassProduction.SchedulerIteration.pointBitWidth dimension width = dimension * width

@[reducible]

noncomputable def Algebraic.MassProduction.SchedulerIteration.lineBitWidth (dimension width : ℕ) : ℕ

Number of packed bits emitted for one punctured line.

Equations

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

@[reducible]

noncomputable def Algebraic.MassProduction.SchedulerIteration.greedyScheduleGateCount {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth : ℕ) : ℕ → ℕ

Total gate count of the recursively unrolled circuit.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.SchedulerIteration.greedyScheduleGateCount dimension widthPositive depth 0 = 0

noncomputable def Algebraic.MassProduction.SchedulerIteration.targetArrayBits {width requests dimension : ℕ} (widthPositive : 0 < width) (targets : Fin requests → Fin dimension → BinaryExtension width) : Fin (requests * pointBitWidth dimension width) → Bool

Row-major target-array encoding.

Equations

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

@[simp]

theorem Algebraic.MassProduction.SchedulerIteration.targetArrayBits_apply {width requests dimension : ℕ} (widthPositive : 0 < width) (targets : Fin requests → Fin dimension → BinaryExtension width) (request : Fin requests) (bit : Fin (pointBitWidth dimension width)) : targetArrayBits widthPositive targets (finProdFinEquiv (request, bit)) = binaryExtensionVectorBits widthPositive (targets request) bit

def Algebraic.MassProduction.SchedulerIteration.targetPrefixInputIndex (requests pointWidth : ℕ) : Fin (requests * pointWidth) → Fin ((requests + 1) * pointWidth)

Map a full target array to its initial request prefix.

Equations

• Algebraic.MassProduction.SchedulerIteration.targetPrefixInputIndex requests pointWidth = Algebraic.MassProduction.blockPrefixIndex

def Algebraic.MassProduction.SchedulerIteration.currentTargetInputIndex (requests pointWidth : ℕ) : Fin pointWidth → Fin ((requests + 1) * pointWidth)

Select the final target from a nonempty target array.

Equations

• Algebraic.MassProduction.SchedulerIteration.currentTargetInputIndex requests pointWidth = Algebraic.MassProduction.blockSuffixIndex

theorem Algebraic.MassProduction.SchedulerIteration.targetPrefixInputIndex_apply {requests pointWidth : ℕ} (request : Fin requests) (bit : Fin pointWidth) : targetPrefixInputIndex requests pointWidth (finProdFinEquiv (request, bit)) = finProdFinEquiv (request.castSucc, bit)

theorem Algebraic.MassProduction.SchedulerIteration.currentTargetInputIndex_apply {pointWidth requests : ℕ} (bit : Fin pointWidth) : currentTargetInputIndex requests pointWidth bit = finProdFinEquiv (Fin.last requests, bit)

theorem Algebraic.MassProduction.SchedulerIteration.targetArrayBits_prefix {width requests dimension : ℕ} (widthPositive : 0 < width) (targets : Fin (requests + 1) → Fin dimension → BinaryExtension width) : targetArrayBits widthPositive targets ∘ targetPrefixInputIndex requests (pointBitWidth dimension width) = targetArrayBits widthPositive fun (request : Fin requests) => targets request.castSucc

theorem Algebraic.MassProduction.SchedulerIteration.targetArrayBits_current {width requests dimension : ℕ} (widthPositive : 0 < width) (targets : Fin (requests + 1) → Fin dimension → BinaryExtension width) : targetArrayBits widthPositive targets ∘ currentTargetInputIndex requests (pointBitWidth dimension width) = binaryExtensionVectorBits widthPositive (targets (Fin.last requests))

noncomputable def Algebraic.MassProduction.SchedulerIteration.greedyStageInputIndex (dimension width depth priorRequests : ℕ) (_priorFits : priorRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (flat : Fin ((Sorting.networkRecords depth + 1) * pointBitWidth dimension width)) : Fin (priorRequests * lineBitWidth dimension width + pointBitWidth dimension width)

Construct the next stage input from the retained prefix-line outputs and the current target. The first priorRequests * (q - 1) point records are live; every remaining point record and the final target record read the current target block.

Equations

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

noncomputable def Algebraic.MassProduction.SchedulerIteration.greedyStageInputCircuit (dimension width depth priorRequests : ℕ) (priorFits : priorRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : Circuit DeMorgan.signature (priorRequests * lineBitWidth dimension width + pointBitWidth dimension width) ((Sorting.networkRecords depth + 1) * pointBitWidth dimension width)

Free rewiring from the retained state to one scheduler-stage input.

Equations

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

@[simp]

theorem Algebraic.MassProduction.SchedulerIteration.greedyStageInputCircuit_size (dimension width depth priorRequests : ℕ) (priorFits : priorRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : (greedyStageInputCircuit dimension width depth priorRequests priorFits).size = 0

greedyStageInputCircuit is pure wiring: it has no gates.

@[simp]

theorem Algebraic.MassProduction.SchedulerIteration.greedyStageInputCircuit_cost {priorRequests width depth dimension : ℕ} (priorFits : priorRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : (greedyStageInputCircuit dimension width depth priorRequests priorFits).cost DeMorgan.standardCost = 0

theorem Algebraic.MassProduction.SchedulerIteration.greedyStageInputIndex_point_of_padding {priorRequests width depth dimension : ℕ} (priorFits : priorRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (record : Fin (Sorting.networkRecords depth)) (bit : Fin (pointBitWidth dimension width)) (padding : ¬↑record < priorRequests * LineEnumeration.nonzeroScalarCount width) : greedyStageInputIndex dimension width depth priorRequests priorFits (SchedulerStage.stagePointInputIndex depth (pointBitWidth dimension width) record bit) = Fin.natAdd (priorRequests * lineBitWidth dimension width) bit

theorem Algebraic.MassProduction.SchedulerIteration.greedyStageInputIndex_target {priorRequests width depth dimension : ℕ} (priorFits : priorRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (bit : Fin (pointBitWidth dimension width)) : greedyStageInputIndex dimension width depth priorRequests priorFits (SchedulerStage.stageTargetInputIndex depth (pointBitWidth dimension width) bit) = Fin.natAdd (priorRequests * lineBitWidth dimension width) bit

noncomputable def Algebraic.MassProduction.SchedulerIteration.greedyStagePoints {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth priorRequests : ℕ) (priorFits : priorRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (state : Fin (priorRequests * lineBitWidth dimension width + pointBitWidth dimension width) → Bool) (record : Fin (Sorting.networkRecords depth)) : Fin dimension → BinaryExtension width

Decode the point presented to one record of the next scheduler stage.

Equations

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

theorem Algebraic.MassProduction.SchedulerIteration.greedyStageInputCircuit_pointBits {width priorRequests depth dimension : ℕ} (widthPositive : 0 < width) (priorFits : priorRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (state : Fin (priorRequests * lineBitWidth dimension width + pointBitWidth dimension width) → Bool) (record : Fin (Sorting.networkRecords depth)) (bit : Fin (pointBitWidth dimension width)) : (greedyStageInputCircuit dimension width depth priorRequests priorFits).eval DeMorgan.interpretation state (SchedulerStage.stagePointInputIndex depth (pointBitWidth dimension width) record bit) = binaryExtensionVectorBits widthPositive (greedyStagePoints dimension widthPositive depth priorRequests priorFits state record) bit

theorem Algebraic.MassProduction.SchedulerIteration.greedyStagePoints_eq_target_of_padding {width priorRequests depth dimension : ℕ} (widthPositive : 0 < width) (priorFits : priorRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (state : Fin (priorRequests * lineBitWidth dimension width + pointBitWidth dimension width) → Bool) (target : Fin dimension → BinaryExtension width) (targetBits : ∀ (bit : Fin (pointBitWidth dimension width)), state (Fin.natAdd (priorRequests * lineBitWidth dimension width) bit) = binaryExtensionVectorBits widthPositive target bit) (record : Fin (Sorting.networkRecords depth)) (padding : ¬↑record < priorRequests * LineEnumeration.nonzeroScalarCount width) : greedyStagePoints dimension widthPositive depth priorRequests priorFits state record = target

theorem Algebraic.MassProduction.SchedulerIteration.greedyStageInputCircuit_targetBits {width priorRequests depth dimension : ℕ} (widthPositive : 0 < width) (priorFits : priorRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (state : Fin (priorRequests * lineBitWidth dimension width + pointBitWidth dimension width) → Bool) (target : Fin dimension → BinaryExtension width) (targetBits : ∀ (bit : Fin (pointBitWidth dimension width)), state (Fin.natAdd (priorRequests * lineBitWidth dimension width) bit) = binaryExtensionVectorBits widthPositive target bit) (bit : Fin (pointBitWidth dimension width)) : (greedyStageInputCircuit dimension width depth priorRequests priorFits).eval DeMorgan.interpretation state (SchedulerStage.stageTargetInputIndex depth (pointBitWidth dimension width) bit) = binaryExtensionVectorBits widthPositive target bit

theorem Algebraic.MassProduction.SchedulerIteration.pointDifferentIndices_greedyStagePoints_card_le {width priorRequests depth dimension : ℕ} (widthPositive : 0 < width) (priorFits : priorRequests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (state : Fin (priorRequests * lineBitWidth dimension width + pointBitWidth dimension width) → Bool) (target : Fin dimension → BinaryExtension width) (targetBits : ∀ (bit : Fin (pointBitWidth dimension width)), state (Fin.natAdd (priorRequests * lineBitWidth dimension width) bit) = binaryExtensionVectorBits widthPositive target bit) : (SchedulerStage.pointDifferentIndices (greedyStagePoints dimension widthPositive depth priorRequests priorFits state) target).card ≤ priorRequests * LineEnumeration.nonzeroScalarCount width

noncomputable def Algebraic.MassProduction.SchedulerIteration.greedyScheduleCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth requests : ℕ) : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth → Circuit DeMorgan.signature (requests * pointBitWidth dimension width) (requests * lineBitWidth dimension width)

Recursively unrolled circuit for a fixed request group. Its output is the request-major concatenation of all enumerated punctured lines.

Equations

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

@[simp]

theorem Algebraic.MassProduction.SchedulerIteration.greedyScheduleCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth requests : ℕ) (fits : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : (greedyScheduleCircuit dimension widthPositive depth requests fits).size = greedyScheduleGateCount dimension widthPositive depth requests

The unrolled scheduler emits exactly greedyScheduleGateCount gates.

Decoding the recursively emitted schedule

theorem Algebraic.MassProduction.SchedulerIteration.priorRequestsFit {requests width depth : ℕ} (allFit : (requests + 1) * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth

Capacity for a request prefix follows from capacity for one additional request. This remains an ordinary proof parameter.

noncomputable def Algebraic.MassProduction.SchedulerIteration.greedyScheduleOutput {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth requests : ℕ) (allFit : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (targets : Fin requests → Fin dimension → BinaryExtension width) : Fin (requests * lineBitWidth dimension width) → Bool

Evaluate the unrolled scheduler on a row-major target array.

Equations

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

noncomputable def Algebraic.MassProduction.SchedulerIteration.scheduledLineBits {requests dimension width : ℕ} (output : Fin (requests * lineBitWidth dimension width) → Bool) (request : Fin requests) : Fin (lineBitWidth dimension width) → Bool

Output bits belonging to one requested line.

Equations

• Algebraic.MassProduction.SchedulerIteration.scheduledLineBits output request = Algebraic.MassProduction.directProductInput output request

noncomputable def Algebraic.MassProduction.SchedulerIteration.scheduledLinePoint {width requests dimension : ℕ} (widthPositive : 0 < width) (output : Fin (requests * lineBitWidth dimension width) → Bool) (request : Fin requests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)) : Fin dimension → BinaryExtension width

Decode one point position of one scheduled line.

Equations

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

noncomputable def Algebraic.MassProduction.SchedulerIteration.scheduledLineSet {width requests dimension : ℕ} (widthPositive : 0 < width) (output : Fin (requests * lineBitWidth dimension width) → Bool) (request : Fin requests) : Finset (Fin dimension → BinaryExtension width)

Decode the recovery set emitted for one request.

Equations

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

def Algebraic.MassProduction.SchedulerIteration.PairwiseDisjointFamily {requests : ℕ} {pointType : Type u_1} (sets : Fin requests → Finset pointType) : Prop

An order-oriented formulation of pairwise disjointness, convenient for the greedy induction.

Equations

• Algebraic.MassProduction.SchedulerIteration.PairwiseDisjointFamily sets = ∀ (earlier later : Fin requests), earlier < later → Disjoint (sets earlier) (sets later)

theorem Algebraic.MassProduction.SchedulerIteration.PairwiseDisjointFamily.disjoint_of_ne {requests : ℕ} {pointType : Type u_1} {sets : Fin requests → Finset pointType} (pairwise : PairwiseDisjointFamily sets) {left right : Fin requests} (different : left ≠ right) : Disjoint (sets left) (sets right)

theorem Algebraic.MassProduction.SchedulerIteration.PairwiseDisjointFamily.snoc {requests : ℕ} {pointType : Type u_1} {sets : Fin requests → Finset pointType} {newSet : Finset pointType} (pairwise : PairwiseDisjointFamily sets) (newDisjoint : ∀ (request : Fin requests), Disjoint (sets request) newSet) : PairwiseDisjointFamily (Fin.snoc sets newSet)

theorem Algebraic.MassProduction.SchedulerIteration.finAppend_comp_castAdd {prefixSize : ℕ} {valueType : Sort u_1} {suffixSize : ℕ} (leftValues : Fin prefixSize → valueType) (rightValues : Fin suffixSize → valueType) : Fin.append leftValues rightValues ∘ Fin.castAdd suffixSize = leftValues

theorem Algebraic.MassProduction.SchedulerIteration.greedyScheduleOutput_succ {requests width depth dimension : ℕ} {widthPositive : 0 < width} (allFit : (requests + 1) * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (targets : Fin (requests + 1) → Fin dimension → BinaryExtension width) : greedyScheduleOutput dimension widthPositive depth (requests + 1) allFit targets = fun (output : Fin (requests.succ * lineBitWidth dimension width)) => Fin.append (greedyScheduleOutput dimension widthPositive depth requests ⋯ fun (request : Fin requests) => targets request.castSucc) ((LineEnumeration.scheduledLineEnumerationCircuit dimension widthPositive depth).eval DeMorgan.interpretation ((greedyStageInputCircuit dimension width depth requests ⋯).eval DeMorgan.interpretation (Fin.append (greedyScheduleOutput dimension widthPositive depth requests ⋯ fun (request : Fin requests) => targets request.castSucc) (binaryExtensionVectorBits widthPositive (targets (Fin.last requests)))))) (Fin.cast ⋯ output)

One unfolding step of the scheduler evaluation: retain the prefix output, append the current target, form the next stage input, and append its line.

theorem Algebraic.MassProduction.SchedulerIteration.cast_succ_mul_finProd_castSucc {requests blockWidth : ℕ} (request : Fin requests) (bit : Fin blockWidth) : Fin.cast ⋯ (finProdFinEquiv (request.castSucc, bit)) = Fin.castAdd blockWidth (finProdFinEquiv (request, bit))

theorem Algebraic.MassProduction.SchedulerIteration.cast_succ_mul_finProd_last {blockWidth requests : ℕ} (bit : Fin blockWidth) : Fin.cast ⋯ (finProdFinEquiv (Fin.last requests, bit)) = Fin.natAdd (requests * blockWidth) bit

theorem Algebraic.MassProduction.SchedulerIteration.scheduledLineBits_greedyScheduleOutput_succ_castSucc {requests width depth dimension : ℕ} {widthPositive : 0 < width} (allFit : (requests + 1) * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (targets : Fin (requests + 1) → Fin dimension → BinaryExtension width) (request : Fin requests) : scheduledLineBits (greedyScheduleOutput dimension widthPositive depth (requests + 1) allFit targets) request.castSucc = scheduledLineBits (greedyScheduleOutput dimension widthPositive depth requests ⋯ fun (prior : Fin requests) => targets prior.castSucc) request

Earlier request blocks are preserved exactly by one recursive stage.

theorem Algebraic.MassProduction.SchedulerIteration.scheduledLineBits_greedyScheduleOutput_succ_last {requests width depth dimension : ℕ} {widthPositive : 0 < width} (allFit : (requests + 1) * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (targets : Fin (requests + 1) → Fin dimension → BinaryExtension width) : scheduledLineBits (greedyScheduleOutput dimension widthPositive depth (requests + 1) allFit targets) (Fin.last requests) = (LineEnumeration.scheduledLineEnumerationCircuit dimension widthPositive depth).eval DeMorgan.interpretation ((greedyStageInputCircuit dimension width depth requests ⋯).eval DeMorgan.interpretation (Fin.append (greedyScheduleOutput dimension widthPositive depth requests ⋯ fun (prior : Fin requests) => targets prior.castSucc) (binaryExtensionVectorBits widthPositive (targets (Fin.last requests)))))

The final request block is exactly the output of the newly evaluated scheduler-and-enumerator stage.

noncomputable def Algebraic.MassProduction.SchedulerIteration.retainedRecordIndex {requests width depth : ℕ} (priorFit : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (request : Fin requests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)) : Fin (Sorting.networkRecords depth)

Location in the fixed power-of-two stage array of one previously emitted line point.

Equations

• Algebraic.MassProduction.SchedulerIteration.retainedRecordIndex priorFit request scalar = ⟨↑(finProdFinEquiv (request, scalar)), ⋯⟩

@[simp]

theorem Algebraic.MassProduction.SchedulerIteration.retainedRecordIndex_val {requests width depth : ℕ} (priorFit : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (request : Fin requests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)) : ↑(retainedRecordIndex priorFit request scalar) = ↑(finProdFinEquiv (request, scalar))

theorem Algebraic.MassProduction.SchedulerIteration.retainedRecordIndex_live {requests width depth : ℕ} (priorFit : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (request : Fin requests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)) : ↑(retainedRecordIndex priorFit request scalar) < requests * LineEnumeration.nonzeroScalarCount width

theorem Algebraic.MassProduction.SchedulerIteration.greedyStageInputIndex_retainedRecord {requests width depth dimension : ℕ} (priorFit : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (request : Fin requests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)) (bit : Fin (pointBitWidth dimension width)) : greedyStageInputIndex dimension width depth requests priorFit (SchedulerStage.stagePointInputIndex depth (pointBitWidth dimension width) (retainedRecordIndex priorFit request scalar) bit) = Fin.castAdd (pointBitWidth dimension width) (finProdFinEquiv (request, finProdFinEquiv (scalar, bit)))

theorem Algebraic.MassProduction.SchedulerIteration.greedyStagePoints_retainedRecord {width requests depth dimension : ℕ} (widthPositive : 0 < width) (priorFit : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (prefixOutput : Fin (requests * lineBitWidth dimension width) → Bool) (target : Fin dimension → BinaryExtension width) (request : Fin requests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)) : greedyStagePoints dimension widthPositive depth requests priorFit (Fin.append prefixOutput (binaryExtensionVectorBits widthPositive target)) (retainedRecordIndex priorFit request scalar) = scheduledLinePoint widthPositive prefixOutput request scalar

Every previously emitted point is decoded identically when retained as a live point of the next scheduler stage.

theorem Algebraic.MassProduction.SchedulerIteration.scheduledLinePoint_mem_greedyStagePointArraySet {width requests depth dimension : ℕ} (widthPositive : 0 < width) (priorFit : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (prefixOutput : Fin (requests * lineBitWidth dimension width) → Bool) (target : Fin dimension → BinaryExtension width) (request : Fin requests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)) : scheduledLinePoint widthPositive prefixOutput request scalar ∈ SchedulerStage.pointArraySet (greedyStagePoints dimension widthPositive depth requests priorFit (Fin.append prefixOutput (binaryExtensionVectorBits widthPositive target)))

theorem Algebraic.MassProduction.SchedulerIteration.scheduledLineSet_subset_greedyStagePointArraySet {width requests depth dimension : ℕ} (widthPositive : 0 < width) (priorFit : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (prefixOutput : Fin (requests * lineBitWidth dimension width) → Bool) (target : Fin dimension → BinaryExtension width) (request : Fin requests) : scheduledLineSet widthPositive prefixOutput request ⊆ SchedulerStage.pointArraySet (greedyStagePoints dimension widthPositive depth requests priorFit (Fin.append prefixOutput (binaryExtensionVectorBits widthPositive target)))

theorem Algebraic.MassProduction.SchedulerIteration.pointDifferentIndices_greedyStageOutput_card_le {width requests depth dimension : ℕ} (widthPositive : 0 < width) (priorFit : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (prefixOutput : Fin (requests * lineBitWidth dimension width) → Bool) (target : Fin dimension → BinaryExtension width) : (SchedulerStage.pointDifferentIndices (greedyStagePoints dimension widthPositive depth requests priorFit (Fin.append prefixOutput (binaryExtensionVectorBits widthPositive target))) target).card ≤ requests * LineEnumeration.nonzeroScalarCount width

Correctness of the unrolled greedy scheduler

theorem Algebraic.MassProduction.SchedulerIteration.greedyScheduleCircuit_correct {width depth dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (requests : ℕ) (allFit : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (capacity : requests * LineEnumeration.nonzeroScalarCount width < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (targets : Fin requests → Fin dimension → BinaryExtension width) : ∃ (directions : Fin requests → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (∀ (request : Fin requests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)), scheduledLinePoint widthPositive (greedyScheduleOutput dimension widthPositive depth requests allFit targets) request scalar = targets request + LineEnumeration.enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector (directions request).rep) ∧ (∀ (request : Fin requests), scheduledLineSet widthPositive (greedyScheduleOutput dimension widthPositive depth requests allFit targets) request = ForbiddenRanks.binaryExtensionPuncturedLine (targets request) (directions request)) ∧ PairwiseDisjointFamily (scheduledLineSet widthPositive (greedyScheduleOutput dimension widthPositive depth requests allFit targets))

The exact constructive greedy scheduler theorem. Each request receives the punctured affine line through its target in an explicitly produced projective direction, and the emitted recovery sets are pairwise disjoint.

Cost of the unrolled scheduler

theorem Algebraic.MassProduction.SchedulerIteration.greedyScheduleCircuit_cost {width depth dimension : ℕ} (widthPositive : 0 < width) (requests : ℕ) (allFit : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : (greedyScheduleCircuit dimension widthPositive depth requests allFit).cost DeMorgan.standardCost = requests * (LineEnumeration.scheduledLineEnumerationCircuit dimension widthPositive depth).cost DeMorgan.standardCost

The recursive scheduler uses one fixed-depth scheduler-and-enumerator stage per request; all retained-state and target wiring is free.

theorem Algebraic.MassProduction.SchedulerIteration.greedyScheduleCircuit_cost_le {width depth dimension : ℕ} (widthPositive : 0 < width) (requests : ℕ) (allFit : requests * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : (greedyScheduleCircuit dimension widthPositive depth requests allFit).cost DeMorgan.standardCost ≤ requests * LineEnumeration.scheduledLineEnumerationCostBound dimension width depth

Explicit finite cost bound corresponding to the manuscript's g stages, each provisioned for g (q - 1) retained points.