Grouped recovery of packed Boolean requests #
This is the semantic junction between the manuscript's packing, geometric scheduler, and bounded-demand grouping. Each request supplies a source information coordinate and a suffix. The grouped scheduler emits a punctured line, and the indicated bit of the field-resource sum is proved to be the original Boolean function value for that request.
theorem
Algebraic.MassProduction.PackedGroupedRecovery.packedGroupedSchedule_recovers
{Prefix : Type u}
{width dimension groups totalRequests depth : ℕ}
{Suffix : Sort u_1}
(widthPositive : 0 < width)
(widthAtLeastTwo : 2 ≤ width)
(dimensionPositive : 0 < dimension)
(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)))
(placement : Prefix ↪ PackedBitPosition dimension width)
(function : Prefix → Suffix → Bool)
(requestSource : Fin totalRequests → Prefix)
(requestSuffix : Fin totalRequests → Suffix)
(dummy : Fin dimension → BinaryExtension width)
:
have targets := fun (request : Fin totalRequests) => packedTargetPoint widthPositive placement (requestSource request);
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),
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),
decodeBinaryExtension widthPositive
(packedEvaluationResource widthPositive placement function
(GroupedScheduler.requestScheduledLinePoint widthPositive capacity output request scalar)
(requestSuffix request))
(placement (requestSource request)).2 = function (requestSource request) (requestSuffix request)
The complete packed, grouped, scheduled recovery invariant.