Incidence keys for concrete scatter routing

Each scheduled (request, nonzero scalar) pair is one incidence. Its routing key is (group, affine point). Within-group line disjointness and within-line scalar injectivity imply that all incidence keys are distinct. The same structured keys index the complete rectangular resource-slot array, giving the exact source-to-destination map required by the verified routing primitive.

@[reducible, inline]

abbrev Algebraic.MassProduction.IncidenceRouting.ResourceSlot (groups dimension width : ℕ) : Type

A resource slot is identified by its request group and affine-space coordinate.

Equations

• Algebraic.MassProduction.IncidenceRouting.ResourceSlot groups dimension width = (Fin groups × (Fin dimension → Algebraic.MassProduction.BinaryExtension width))

noncomputable def Algebraic.MassProduction.IncidenceRouting.scheduledIncidenceSlot {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (capacity : totalRequests ≤ groups * requestsPerGroup) (output : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (incidence : Fin totalRequests × Fin (LineEnumeration.nonzeroScalarCount width)) : ResourceSlot groups dimension width

Structured slot requested by one scheduled line incidence.

Equations

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

theorem Algebraic.MassProduction.IncidenceRouting.requestScheduledLinePoint_mem_set {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)) : GroupedScheduler.requestScheduledLinePoint widthPositive capacity output request scalar ∈ GroupedScheduler.requestScheduledLineSet widthPositive capacity output request

Every scalar-indexed point belongs to its decoded request recovery set.

theorem Algebraic.MassProduction.IncidenceRouting.scheduledIncidenceSlot_injective {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) (withinGroupDisjoint : ∀ (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)) : Function.Injective (scheduledIncidenceSlot widthPositive capacity output)

The scheduled (group, point) incidence keys are injective.

noncomputable def Algebraic.MassProduction.IncidenceRouting.resourceSlotEquiv (groups dimension width : ℕ) : ResourceSlot groups dimension width ≃ Fin (Nat.card (ResourceSlot groups dimension width))

A fixed finite enumeration of all resource slots. The particular order is irrelevant here; it reuses the existing Finite structure without installing a Fintype instance.

Equations

• Algebraic.MassProduction.IncidenceRouting.resourceSlotEquiv groups dimension width = Finite.equivFin (Algebraic.MassProduction.IncidenceRouting.ResourceSlot groups dimension width)

noncomputable def Algebraic.MassProduction.IncidenceRouting.resourceSlotAt {groups dimension width : ℕ} (destination : Fin (Nat.card (ResourceSlot groups dimension width))) : ResourceSlot groups dimension width

Structured resource slot at one canonical destination index.

Equations

• Algebraic.MassProduction.IncidenceRouting.resourceSlotAt destination = (Algebraic.MassProduction.IncidenceRouting.resourceSlotEquiv groups dimension width).symm destination

noncomputable def Algebraic.MassProduction.IncidenceRouting.resourceSlotIndex {groups dimension width : ℕ} (slot : ResourceSlot groups dimension width) : Fin (Nat.card (ResourceSlot groups dimension width))

Destination index of a structured resource slot.

Equations

• Algebraic.MassProduction.IncidenceRouting.resourceSlotIndex slot = (Algebraic.MassProduction.IncidenceRouting.resourceSlotEquiv groups dimension width) slot

@[simp]

theorem Algebraic.MassProduction.IncidenceRouting.resourceSlotAt_index {groups dimension width : ℕ} (slot : ResourceSlot groups dimension width) : resourceSlotAt (resourceSlotIndex slot) = slot

@[simp]

theorem Algebraic.MassProduction.IncidenceRouting.resourceSlotIndex_at {groups dimension width : ℕ} (destination : Fin (Nat.card (ResourceSlot groups dimension width))) : resourceSlotIndex (resourceSlotAt destination) = destination

noncomputable def Algebraic.MassProduction.IncidenceRouting.incidenceAt {totalRequests width : ℕ} (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : Fin totalRequests × Fin (LineEnumeration.nonzeroScalarCount width)

Flat row-major incidence index decoded as (request, scalar).

Equations

• Algebraic.MassProduction.IncidenceRouting.incidenceAt incidence = finProdFinEquiv.symm incidence

@[simp]

theorem Algebraic.MassProduction.IncidenceRouting.incidenceAt_finProdFinEquiv {totalRequests width : ℕ} (request : Fin totalRequests) (scalar : Fin (LineEnumeration.nonzeroScalarCount width)) : incidenceAt (finProdFinEquiv (request, scalar)) = (request, scalar)

noncomputable def Algebraic.MassProduction.IncidenceRouting.scheduledIncidenceSlotAt {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (capacity : totalRequests ≤ groups * requestsPerGroup) (output : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : ResourceSlot groups dimension width

Complete structured slot key of one flat incidence.

Equations

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

@[simp]

theorem Algebraic.MassProduction.IncidenceRouting.scheduledIncidenceSlotAt_finProdFinEquiv_first {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)) : (scheduledIncidenceSlotAt widthPositive capacity output (finProdFinEquiv (request, scalar))).1 = (GroupedScheduler.requestGroupSlot capacity request).1

@[simp]

theorem Algebraic.MassProduction.IncidenceRouting.scheduledIncidenceSlotAt_finProdFinEquiv_second {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)) : (scheduledIncidenceSlotAt widthPositive capacity output (finProdFinEquiv (request, scalar))).2 = GroupedScheduler.requestScheduledLinePoint widthPositive capacity output request scalar

theorem Algebraic.MassProduction.IncidenceRouting.scheduledIncidenceSlotAt_injective {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) (withinGroupDisjoint : ∀ (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)) : Function.Injective (scheduledIncidenceSlotAt widthPositive capacity output)

Flat incidence keys inherit injectivity from the structured schedule.

Concrete Boolean routing keys and destinations

@[reducible]

def Algebraic.MassProduction.IncidenceRouting.incidenceKeyWidth (groupBitWidth dimension width : ℕ) : ℕ

Width of an active/padding marker followed by group and affine-point bits.

Equations

• Algebraic.MassProduction.IncidenceRouting.incidenceKeyWidth groupBitWidth dimension width = groupBitWidth + dimension * width + 1

noncomputable def Algebraic.MassProduction.IncidenceRouting.scheduledIncidenceKeyBits {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (output : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : Fin (incidenceKeyWidth groupBitWidth dimension width) → Bool

Concrete marked Boolean key of a scheduled incidence.

Equations

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

noncomputable def Algebraic.MassProduction.IncidenceRouting.resourceDestinationKeyBits {width groups dimension : ℕ} (widthPositive : 0 < width) (groupBitWidth : ℕ) (destination : Fin (Nat.card (ResourceSlot groups dimension width))) : Fin (incidenceKeyWidth groupBitWidth dimension width) → Bool

Every structured resource slot occurs once in the destination array.

Equations

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

noncomputable def Algebraic.MassProduction.IncidenceRouting.incidenceDestination {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (capacity : totalRequests ≤ groups * requestsPerGroup) (output : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : Fin (Nat.card (ResourceSlot groups dimension width))

Destination index corresponding to one scheduled incidence.

Equations

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

def Algebraic.MassProduction.IncidenceRouting.incidencePaddingKey (groupBitWidth dimension width : ℕ) : Fin (incidenceKeyWidth groupBitWidth dimension width) → Bool

All padding records share the reserved padding-marker key. Repetition among padding records is harmless because active destination keys use the opposite marker.

Equations

• Algebraic.MassProduction.IncidenceRouting.incidencePaddingKey groupBitWidth dimension width = Algebraic.MassProduction.paddingRoutingKey fun (x : Fin (groupBitWidth + dimension * width)) => false

theorem Algebraic.MassProduction.IncidenceRouting.scheduledIncidenceKeyBits_injective {width groups groupBitWidth totalRequests requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (groupFits : groups ≤ 2 ^ groupBitWidth) (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) (withinGroupDisjoint : ∀ (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)) : Function.Injective (scheduledIncidenceKeyBits widthPositive groupBitWidth capacity output)

theorem Algebraic.MassProduction.IncidenceRouting.resourceDestinationKeyBits_injective {width groups groupBitWidth dimension : ℕ} (widthPositive : 0 < width) (groupFits : groups ≤ 2 ^ groupBitWidth) : Function.Injective (resourceDestinationKeyBits widthPositive groupBitWidth)

@[simp]

theorem Algebraic.MassProduction.IncidenceRouting.resourceDestinationKeyBits_incidenceDestination {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (output : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : resourceDestinationKeyBits widthPositive groupBitWidth (incidenceDestination widthPositive capacity output incidence) = scheduledIncidenceKeyBits widthPositive groupBitWidth capacity output incidence

theorem Algebraic.MassProduction.IncidenceRouting.incidencePaddingKey_avoids {groupBitWidth dimension width : ℕ} (active : Fin (groupBitWidth + dimension * width) → Bool) : incidencePaddingKey groupBitWidth dimension width ≠ activeRoutingKey active

noncomputable def Algebraic.MassProduction.IncidenceRouting.incidenceSourcePayload {totalRequests payloadWidth width : ℕ} (requestPayload : Fin totalRequests → Fin payloadWidth → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : Fin payloadWidth → Bool

Suffix payload carried by one flat scheduled incidence.

Equations

• Algebraic.MassProduction.IncidenceRouting.incidenceSourcePayload requestPayload incidence = requestPayload (Algebraic.MassProduction.IncidenceRouting.incidenceAt incidence).1

noncomputable def Algebraic.MassProduction.IncidenceRouting.scatterRoutingInputBits {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 (Nat.card (ResourceSlot groups dimension width)) → Fin payloadWidth → Bool) (paddingPayload : Fin paddingCount → Fin payloadWidth → Bool) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + Nat.card (ResourceSlot groups dimension width) + paddingCount = Sorting.networkRecords routingDepth) : Fin (Sorting.networkBits routingDepth (Routing.recordWidth (incidenceKeyWidth groupBitWidth dimension width) payloadWidth)) → Bool

Fully packed scatter input: scheduled incidences, one destination record for every (group, point) slot, and reserved-marker padding records.

Equations

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

theorem Algebraic.MassProduction.IncidenceRouting.scatterRoutingInputBits_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 (Nat.card (ResourceSlot groups dimension width)) → Fin payloadWidth → Bool) (paddingPayload : Fin paddingCount → Fin payloadWidth → Bool) (recordCount : totalRequests * LineEnumeration.nonzeroScalarCount width + Nat.card (ResourceSlot groups dimension width) + paddingCount = Sorting.networkRecords routingDepth) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : have input := scatterRoutingInputBits widthPositive groupBitWidth capacity scheduleOutput requestPayload destinationPayload paddingPayload recordCount; have sorted := Sorting.bitonicSortBits ⋯ routingDepth true input; ∃ (destinationSorted : Fin (Sorting.networkRecords routingDepth)), Routing.recordHasKeyTag (scheduledIncidenceKeyBits widthPositive groupBitWidth capacity scheduleOutput incidence) true (Sorting.flatRecords sorted destinationSorted) ∧ Routing.recordPayload ((Routing.sortedPredecessorCopyCircuit routingDepth (incidenceKeyWidth groupBitWidth dimension width) payloadWidth false true).eval DeMorgan.interpretation input) destinationSorted = requestPayload (incidenceAt incidence).1

Concrete scatter theorem. Every scheduled incidence sends exactly its request suffix to the destination indexed by the incidence's (group, point) slot key.

Full key-space slot arrays for canonical ordering

noncomputable def Algebraic.MassProduction.IncidenceRouting.fullResourceDestinationKeyBits (groupBitWidth dimension width : ℕ) (destination : Fin (2 ^ (groupBitWidth + dimension * width))) : Fin (incidenceKeyWidth groupBitWidth dimension width) → Bool

Destination key at a canonical lexicographic position in the complete unmarked key space. Provisioning the full key space costs at most the usual power-of-two rounding factor once groupBitWidth is chosen minimally.

Equations

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

noncomputable def Algebraic.MassProduction.IncidenceRouting.fullIncidenceDestination {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (output : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : Fin (2 ^ (groupBitWidth + dimension * width))

Canonical full-key-space destination of one scheduled incidence.

Equations

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

theorem Algebraic.MassProduction.IncidenceRouting.fullResourceDestinationKeyBits_injective {groupBitWidth dimension width : ℕ} : Function.Injective (fullResourceDestinationKeyBits groupBitWidth dimension width)

@[simp]

theorem Algebraic.MassProduction.IncidenceRouting.fullResourceDestinationKeyBits_fullIncidenceDestination {width totalRequests groups requestsPerGroup dimension : ℕ} (widthPositive : 0 < width) (groupBitWidth : ℕ) (capacity : totalRequests ≤ groups * requestsPerGroup) (output : Fin (groups * (requestsPerGroup * SchedulerIteration.lineBitWidth dimension width)) → Bool) (incidence : Fin (totalRequests * LineEnumeration.nonzeroScalarCount width)) : fullResourceDestinationKeyBits groupBitWidth dimension width (fullIncidenceDestination widthPositive groupBitWidth capacity output incidence) = scheduledIncidenceKeyBits widthPositive groupBitWidth capacity output incidence

noncomputable def Algebraic.MassProduction.IncidenceRouting.fullScatterRoutingInputBits {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 (incidenceKeyWidth groupBitWidth dimension width) payloadWidth)) → Bool

Packed scatter input with one destination for every possible active key. This variant makes the destination prefix after canonical sorting completely independent of the run-time incidence subset.

Equations

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

theorem Algebraic.MassProduction.IncidenceRouting.fullScatterRoutingInputBits_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 input := fullScatterRoutingInputBits widthPositive groupBitWidth capacity scheduleOutput requestPayload destinationPayload paddingPayload recordCount; have sorted := Sorting.bitonicSortBits ⋯ routingDepth true input; ∃ (destinationSorted : Fin (Sorting.networkRecords routingDepth)), Routing.recordHasKeyTag (scheduledIncidenceKeyBits widthPositive groupBitWidth capacity scheduleOutput incidence) true (Sorting.flatRecords sorted destinationSorted) ∧ Routing.recordPayload ((Routing.sortedPredecessorCopyCircuit routingDepth (incidenceKeyWidth groupBitWidth dimension width) payloadWidth false true).eval DeMorgan.interpretation input) destinationSorted = requestPayload (incidenceAt incidence).1

Every incidence is routed correctly in the full-key-space scatter layout.