Recovery from padded request groups

This module combines arbitrary-count request grouping with the generic punctured-line recovery interface. The resource may depend on the request; this is essential because different mass-production requests carry different suffix inputs while querying the same family of shorter resource functions.

theorem Algebraic.MassProduction.GroupedRecovery.requestScheduledLinePoint_injective_of_formula {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (capacity : totalRequests ≤ groups * requestsPerGroup) (output : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (targets : Fin totalRequests → Fin dimension → BinaryExtension width) (directions : Fin totalRequests → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (pointFormula : ∀ (request : Fin totalRequests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)), GroupedScheduler.requestScheduledLinePoint widthPositive capacity output request scalar = targets request + LineEnumeration.enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector (directions request).rep) (request : Fin totalRequests) : Function.Injective (GroupedScheduler.requestScheduledLinePoint widthPositive capacity output request)

A pointwise affine-line formula makes the scalar-indexed points for one real request injective.

theorem Algebraic.MassProduction.GroupedRecovery.sum_requestScheduledLinePoint_eq_set {width totalRequests groups requestsPerGroup dimension : ℕ} {valueType : Type u_1} [AddCommMonoid valueType] (widthPositive : 0 < width) (capacity : totalRequests ≤ groups * requestsPerGroup) (output : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (resource : (Fin dimension → BinaryExtension width) → valueType) (request : Fin totalRequests) (injective : Function.Injective (GroupedScheduler.requestScheduledLinePoint widthPositive capacity output request)) : ∑ scalar : Fin (LineEnumeration.nonzeroScalarCount width), resource (GroupedScheduler.requestScheduledLinePoint widthPositive capacity output request scalar) = ∑ point ∈ GroupedScheduler.requestScheduledLineSet widthPositive capacity output request, resource point

The scalar-indexed request output and its decoded finite set carry the same resource sum.

theorem Algebraic.MassProduction.GroupedRecovery.paddedGroupedScheduleCircuit_recovers {width groups totalRequests depth dimension : ℕ} {valueType : Type u_1} [AddCommMonoid valueType] (widthPositive : 0 < width) (widthAtLeastTwo : 2 ≤ width) (groupsPositive : 0 < groups) (allFit : GroupedScheduler.requestGroupSize totalRequests groups * LineEnumeration.nonzeroScalarCount width ≤ Sorting.networkRecords depth) (directionCapacity : GroupedScheduler.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) (resource : Fin totalRequests → (Fin dimension → BinaryExtension width) → valueType) (lineRecovery : ∀ (request : Fin totalRequests) (direction : Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)), resource request (targets request) = ∑ point ∈ ForbiddenRanks.binaryExtensionPuncturedLine (targets request) direction, resource request point) : let groupSize := GroupedScheduler.requestGroupSize totalRequests groups; have capacity := ⋯; have paddedTargets := GroupedScheduler.paddedGroupedTargets capacity targets dummy; have output := GroupedScheduler.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)), GroupedScheduler.requestScheduledLinePoint widthPositive capacity output request scalar = targets request + LineEnumeration.enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector (directions request).rep) ∧ (∀ (request : Fin totalRequests), GroupedScheduler.requestScheduledLineSet widthPositive capacity output request = ForbiddenRanks.binaryExtensionPuncturedLine (targets request) (directions request)) ∧ (∀ (left right : Fin totalRequests), (GroupedScheduler.requestGroupSlot capacity left).1 = (GroupedScheduler.requestGroupSlot capacity right).1 → left ≠ right → Disjoint (GroupedScheduler.requestScheduledLineSet widthPositive capacity output left) (GroupedScheduler.requestScheduledLineSet widthPositive capacity output right)) ∧ ∀ (request : Fin totalRequests), ∑ scalar : Fin (LineEnumeration.nonzeroScalarCount width), resource request (GroupedScheduler.requestScheduledLinePoint widthPositive capacity output request scalar) = resource request (targets request)

Exact recovery for arbitrary request counts split among positive groups. Only requests assigned to the same group are required to have disjoint recovery sets; every request may carry its own resource evaluation function.