Fixed-wire incidence scatter

This module closes the positional gap in the concrete scatter pass. The first verified sort routes each request suffix to its unique (group, point) destination. The second verified sort places the complete active resource key space in canonical lexicographic order. Consequently each incidence's payload appears on the literal, input-independent wire indexed by its encoded resource slot.

noncomputable def Algebraic.MassProduction.CanonicalScatter.canonicalFullScatterBits {width totalRequests groups requestsPerGroup dimension payloadWidth paddingCount routingDepth : ℕ} (widthPositive : 0 < width) (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (requestPayload : Fin totalRequests → Fin payloadWidth → Bool) (destinationPayload : Fin (2 ^ (groupBitWidth + dimension * width)) → Fin payloadWidth → Bool) (paddingPayload : Fin paddingCount → Fin payloadWidth → Bool) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords routingDepth) : Fin (Sorting.networkBits routingDepth (Routing.recordWidth (IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width) payloadWidth)) → Bool

Full scatter followed by canonical destination ordering.

Equations

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

theorem Algebraic.MassProduction.CanonicalScatter.canonicalFullScatterBits_routes_incidence {width groups groupBitWidth totalRequests requestsPerGroup dimension payloadWidth paddingCount routingDepth : ℕ} (widthPositive : 0 < width) (groupFits : groups ≤ 2 ^ groupBitWidth) (capacity : totalRequests ≤ groups * requestsPerGroup) (scheduleOutput : 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 scheduleOutput request scalar = targets request + LineEnumeration.enumeratedNonzeroScalar scalar • normalizeBinaryExtensionVector (directions request).rep) (withinGroupDisjoint : ∀ (left right : Fin totalRequests), (GroupedScheduler.requestGroupSlot capacity left).1 = (GroupedScheduler.requestGroupSlot capacity right).1 → left ≠ right → Disjoint (GroupedScheduler.requestScheduledLineSet widthPositive capacity scheduleOutput left) (GroupedScheduler.requestScheduledLineSet widthPositive capacity scheduleOutput right)) (requestPayload : Fin totalRequests → Fin payloadWidth → Bool) (destinationPayload : Fin (2 ^ (groupBitWidth + dimension * width)) → Fin payloadWidth → Bool) (paddingPayload : Fin paddingCount → Fin payloadWidth → Bool) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + 2 ^ (groupBitWidth + dimension * width) + paddingCount = Sorting.networkRecords routingDepth) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : have destination := IncidenceRouting.fullIncidenceDestination widthPositive groupBitWidth capacity scheduleOutput incidence; have destinationFits := ⋯; Routing.recordPayload (canonicalFullScatterBits widthPositive groupBitWidth capacity scheduleOutput requestPayload destinationPayload paddingPayload recordCount) (Fin.castLE destinationFits destination) = requestPayload (IncidenceRouting.incidenceAt incidence).1

Every scheduled incidence lands at its fixed full-key-space destination wire with exactly its request payload.