Parallel request-group scheduling

The manuscript permits a resource coordinate to be reused across different request groups, while requiring punctured recovery lines to be disjoint inside each group. This module realizes that exact rectangular construction by replicating the verified greedy scheduler on disjoint group input blocks.

The group count and group size are ordinary natural parameters. In particular, no finite-type or field instances are exported by this layer.

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

Row-major target bits for a rectangular (group, request) family.

Equations

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

@[simp]

theorem Algebraic.MassProduction.GroupedScheduler.directProductInput_groupedTargetArrayBits {width groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (targets : Fin groups → Fin requestsPerGroup → Fin dimension → BinaryExtension width) (group : Fin groups) : directProductInput (groupedTargetArrayBits widthPositive targets) group = SchedulerIteration.targetArrayBits widthPositive (targets group)

noncomputable def Algebraic.MassProduction.GroupedScheduler.groupedScheduleCircuit {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth groups requestsPerGroup : ℕ) (allFit : requestsPerGroup * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : Circuit DeMorgan.signature (groups * (requestsPerGroup * SchedulerIteration.pointBitWidth dimension width)) (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width))

One independent greedy scheduler per request group.

Equations

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

@[simp]

theorem Algebraic.MassProduction.GroupedScheduler.groupedScheduleCircuit_size {width : ℕ} (dimension : ℕ) (widthPositive : 0 < width) (depth groups requestsPerGroup : ℕ) (allFit : requestsPerGroup * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : (groupedScheduleCircuit dimension widthPositive depth groups requestsPerGroup allFit).size = groups * SchedulerIteration.greedyScheduleGateCount dimension widthPositive depth requestsPerGroup

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

Evaluate all group schedulers on the rectangular target family.

Equations

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

noncomputable def Algebraic.MassProduction.GroupedScheduler.groupScheduleBits {groups requestsPerGroup dimension width : ℕ} (output : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (group : Fin groups) : Fin (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width) → Bool

Select the schedule-output block belonging to one group.

Equations

• Algebraic.MassProduction.GroupedScheduler.groupScheduleBits output group = Algebraic.MassProduction.directProductInput output group

theorem Algebraic.MassProduction.GroupedScheduler.groupScheduleBits_groupedScheduleOutput {width requestsPerGroup depth groups dimension : ℕ} (widthPositive : 0 < width) (allFit : requestsPerGroup * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (targets : Fin groups → Fin requestsPerGroup → Fin dimension → BinaryExtension width) (group : Fin groups) : groupScheduleBits (groupedScheduleOutput dimension widthPositive depth groups requestsPerGroup allFit targets) group = SchedulerIteration.greedyScheduleOutput dimension widthPositive depth requestsPerGroup allFit (targets group)

Replication evaluates the verified one-group scheduler independently on the selected group target block.

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

Exact grouped scheduler invariant: every output is a punctured affine line through its target, and lines are pairwise disjoint within each group. No disjointness is asserted across groups, matching the bounded-demand construction.

theorem Algebraic.MassProduction.GroupedScheduler.groupedScheduleCircuit_cost {width requestsPerGroup depth dimension groups : ℕ} (widthPositive : 0 < width) (allFit : requestsPerGroup * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : (groupedScheduleCircuit dimension widthPositive depth groups requestsPerGroup allFit).cost DeMorgan.standardCost = groups * (SchedulerIteration.greedyScheduleCircuit dimension widthPositive depth requestsPerGroup allFit).cost DeMorgan.standardCost

Replication charges exactly one scheduler cost per group.

theorem Algebraic.MassProduction.GroupedScheduler.groupedScheduleCircuit_cost_le {width requestsPerGroup depth dimension groups : ℕ} (widthPositive : 0 < width) (allFit : requestsPerGroup * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) : (groupedScheduleCircuit dimension widthPositive depth groups requestsPerGroup allFit).cost DeMorgan.standardCost ≤ groups * requestsPerGroup * LineEnumeration.scheduledLineEnumerationCostBound dimension width depth

The finite grouped cost ledger: groups * requestsPerGroup copies of the fixed-capacity scheduler/enumerator stage.

Padding an arbitrary request count into fixed groups

def Algebraic.MassProduction.GroupedScheduler.requestGroupSize (totalRequests groups : ℕ) : ℕ

Maximum group size for totalRequests requests split over a positive number of groups.

Equations

• Algebraic.MassProduction.GroupedScheduler.requestGroupSize totalRequests groups = totalRequests ⌈/⌉ groups

theorem Algebraic.MassProduction.GroupedScheduler.requestGroupCapacity {groups totalRequests : ℕ} (groupsPositive : 0 < groups) : totalRequests ≤ groups * requestGroupSize totalRequests groups

The rectangular group array has room for every real request.

def Algebraic.MassProduction.GroupedScheduler.requestGroupSlot {totalRequests groups requestsPerGroup : ℕ} (capacity : totalRequests ≤ groups * requestsPerGroup) (request : Fin totalRequests) : Fin groups × Fin requestsPerGroup

Rectangular (group, local request) position assigned to one real request by row-major order.

Equations

• Algebraic.MassProduction.GroupedScheduler.requestGroupSlot capacity request = finProdFinEquiv.symm (Fin.castLE capacity request)

def Algebraic.MassProduction.GroupedScheduler.paddedGroupedTargets {totalRequests groups requestsPerGroup : ℕ} {pointType : Sort u_1} (_capacity : totalRequests ≤ groups * requestsPerGroup) (targets : Fin totalRequests → pointType) (dummy : pointType) : Fin groups → Fin requestsPerGroup → pointType

Pad unused rectangular request slots with an arbitrary fixed target.

Equations

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

@[simp]

theorem Algebraic.MassProduction.GroupedScheduler.paddedGroupedTargets_at_request {totalRequests groups requestsPerGroup : ℕ} {pointType : Sort u_1} (capacity : totalRequests ≤ groups * requestsPerGroup) (targets : Fin totalRequests → pointType) (dummy : pointType) (request : Fin totalRequests) : paddedGroupedTargets capacity targets dummy (requestGroupSlot capacity request).1 (requestGroupSlot capacity request).2 = targets request

Padding leaves every real request at its assigned rectangular slot.

noncomputable def Algebraic.MassProduction.GroupedScheduler.requestScheduledLinePoint {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (capacity : totalRequests ≤ groups * requestsPerGroup) (output : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (request : Fin totalRequests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)) : Fin dimension → BinaryExtension width

Decode one real request's point from the padded grouped output.

Equations

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

noncomputable def Algebraic.MassProduction.GroupedScheduler.requestScheduledLineSet {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (capacity : totalRequests ≤ groups * requestsPerGroup) (output : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (request : Fin totalRequests) : Finset (Fin dimension → BinaryExtension width)

Recovery set decoded for one real request in a padded grouped output.

Equations

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

theorem Algebraic.MassProduction.GroupedScheduler.paddedGroupedScheduleCircuit_correct {width groups totalRequests depth dimension : ℕ} (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (groupsPositive : 0 < groups) (allFit : requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (directionCapacity : requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width < Nat.card (Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width))) (targets : Fin totalRequests → Fin dimension → BinaryExtension width) (dummy : Fin dimension → BinaryExtension width) : let groupSize := requestGroupSize totalRequests groups; have capacity := ⋯; have paddedTargets := paddedGroupedTargets capacity targets dummy; have output := groupedScheduleOutput dimension widthPositive depth groups groupSize allFit paddedTargets; ∃ (directions : Fin totalRequests → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), (∀ (request : Fin totalRequests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)), requestScheduledLinePoint widthPositive capacity output request scalar = targets request + LineEnumeration.enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector (directions request).rep) ∧ (∀ (request : Fin totalRequests), requestScheduledLineSet widthPositive capacity output request = ForbiddenRanks.binaryExtensionPuncturedLine (targets request) (directions request)) ∧ ∀ (left right : Fin totalRequests), (requestGroupSlot capacity left).1 = (requestGroupSlot capacity right).1 → left ≠ right → Disjoint (requestScheduledLineSet widthPositive capacity output left) (requestScheduledLineSet widthPositive capacity output right)

Arbitrary request counts inherit exact line recovery and within-group disjointness after padding to groups * ceil(totalRequests / groups) slots.