Concrete scatter and gather record packing

This module supplies the record-layout layer omitted by the generic routing primitive. A record is laid out as (key, tag, payload). Source records use tag false, destination records use tag true, and padding records are required to use keys outside the active destination-key image.

The key and payload encodings are explicit functions, not typeclass-driven serializers. This keeps all finite encodings visible in theorem hypotheses.

def Algebraic.MassProduction.Routing.packRecord {keyWidth payloadWidth : ℕ} (key : Fin keyWidth → Bool) (tag : Bool) (payload : Fin payloadWidth → Bool) : Fin (recordWidth keyWidth payloadWidth) → Bool

Pack one standalone (key, tag, payload) record.

Equations

• Algebraic.MassProduction.Routing.packRecord key tag payload = Fin.append (Fin.append key fun (x : Fin 1) => tag) payload

@[simp]

theorem Algebraic.MassProduction.Routing.packedRecordKey_packRecord {keyWidth payloadWidth : ℕ} (key : Fin keyWidth → Bool) (tag : Bool) (payload : Fin payloadWidth → Bool) : packedRecordKey (packRecord key tag payload) = key

@[simp]

theorem Algebraic.MassProduction.Routing.packedRecordTag_packRecord {keyWidth payloadWidth : ℕ} (key : Fin keyWidth → Bool) (tag : Bool) (payload : Fin payloadWidth → Bool) : packedRecordTag (packRecord key tag payload) = tag

@[simp]

theorem Algebraic.MassProduction.Routing.packedRecordPayload_packRecord {keyWidth payloadWidth : ℕ} (key : Fin keyWidth → Bool) (tag : Bool) (payload : Fin payloadWidth → Bool) : packedRecordPayload (packRecord key tag payload) = payload

def Algebraic.MassProduction.Routing.routingRecordSequence {sourceCount keyWidth payloadWidth destinationCount paddingCount : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) : Fin (sourceCount + destinationCount + paddingCount) → Fin (recordWidth keyWidth payloadWidth) → Bool

Concatenate incidence/source records, slot/destination records, and padding records in a fixed initial layout.

Equations

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

theorem Algebraic.MassProduction.Routing.UniqueIndexWhere.append_left {leftCount : ℕ} {α : Sort u_1} {rightCount : ℕ} {left : Fin leftCount → α} {right : Fin rightCount → α} {predicate : α → Prop} (uniqueLeft : UniqueIndexWhere left predicate) (noneRight : ∀ (index : Fin rightCount), ¬predicate (right index)) : UniqueIndexWhere (Fin.append left right) predicate

Routing-namespace compatibility theorem for preserving a unique left match when a match-free right sequence is appended.

theorem Algebraic.MassProduction.Routing.UniqueIndexWhere.append_right {leftCount : ℕ} {α : Sort u_1} {rightCount : ℕ} {left : Fin leftCount → α} {right : Fin rightCount → α} {predicate : α → Prop} (noneLeft : ∀ (index : Fin leftCount), ¬predicate (left index)) (uniqueRight : UniqueIndexWhere right predicate) : UniqueIndexWhere (Fin.append left right) predicate

Routing-namespace compatibility theorem for the symmetric right-match append rule.

theorem Algebraic.MassProduction.Routing.UniqueIndexWhere.cast {leftCount : ℕ} {α : Sort u_1} {rightCount : ℕ} {sequence : Fin leftCount → α} {predicate : α → Prop} (unique : UniqueIndexWhere sequence predicate) (countEquality : leftCount = rightCount) : UniqueIndexWhere (fun (index : Fin rightCount) => sequence (Fin.cast ⋯ index)) predicate

Routing-namespace compatibility theorem for reindexing a unique match along an equality of lengths.

theorem Algebraic.MassProduction.Routing.sourceRecordSequence_unique {sourceCount keyWidth payloadWidth : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (sourceKeysInjective : Function.Injective sourceKeys) (source : Fin sourceCount) : UniqueIndexWhere (fun (index : Fin sourceCount) => packRecord (sourceKeys index) false (sourcePayloads index)) (recordHasKeyTag (sourceKeys source) false)

theorem Algebraic.MassProduction.Routing.destinationRecordSequence_unique {destinationCount keyWidth payloadWidth : ℕ} (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (destinationKeysInjective : Function.Injective destinationKeys) (destination : Fin destinationCount) : UniqueIndexWhere (fun (index : Fin destinationCount) => packRecord (destinationKeys index) true (destinationPayloads index)) (recordHasKeyTag (destinationKeys destination) true)

theorem Algebraic.MassProduction.Routing.routingRecordSequence_unique_key {sourceCount keyWidth payloadWidth destinationCount paddingCount : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (sourceKeysInjective : Function.Injective sourceKeys) (destinationKeysInjective : Function.Injective destinationKeys) (destinationFor : Fin sourceCount → Fin destinationCount) (destinationKey : ∀ (source : Fin sourceCount), destinationKeys (destinationFor source) = sourceKeys source) (paddingAvoids : ∀ (padding : Fin paddingCount) (source : Fin sourceCount), paddingKeys padding ≠ sourceKeys source) (source : Fin sourceCount) : UniqueIndexWhere (routingRecordSequence sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads) (recordHasKeyTag (sourceKeys source) false) ∧ UniqueIndexWhere (routingRecordSequence sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads) (recordHasKeyTag (sourceKeys source) true)

Every active source key has exactly one source record and exactly one destination record in the complete initial routing layout. Injectivity is requested only of the two active key families; padding records may repeat one another, but their keys must avoid every active source key.

theorem Algebraic.MassProduction.Routing.routingRecordSequence_unique_destination {sourceCount keyWidth payloadWidth destinationCount paddingCount : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (destinationKeysInjective : Function.Injective destinationKeys) (paddingAvoidsDestination : ∀ (padding : Fin paddingCount) (destination : Fin destinationCount), paddingKeys padding ≠ destinationKeys destination) (destination : Fin destinationCount) : UniqueIndexWhere (routingRecordSequence sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads) (recordHasKeyTag (destinationKeys destination) true)

Every destination key is unique in the complete layout independently of whether a matching source with that key exists.

theorem Algebraic.MassProduction.Routing.routingRecordSequence_unique_source {sourceCount keyWidth payloadWidth destinationCount paddingCount : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (sourceKeysInjective : Function.Injective sourceKeys) (source : Fin sourceCount) : UniqueIndexWhere (routingRecordSequence sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads) (recordHasKeyTag (sourceKeys source) false)

Every source key is unique in the complete layout whenever the source-key family is injective. Destination and padding keys are irrelevant because their tag is different.

Exact network-capacity padding

def Algebraic.MassProduction.Routing.routingSourceIndex {sourceCount destinationCount paddingCount : ℕ} (source : Fin sourceCount) : Fin (sourceCount + destinationCount + paddingCount)

Position occupied by a source record in the unpadded semantic layout.

Equations

• Algebraic.MassProduction.Routing.routingSourceIndex source = Fin.castAdd paddingCount (Fin.castAdd destinationCount source)

def Algebraic.MassProduction.Routing.routingDestinationIndex {destinationCount sourceCount paddingCount : ℕ} (destination : Fin destinationCount) : Fin (sourceCount + destinationCount + paddingCount)

Position occupied by a destination record in the unpadded semantic routing layout.

Equations

• Algebraic.MassProduction.Routing.routingDestinationIndex destination = Fin.castAdd paddingCount (Fin.natAdd sourceCount destination)

def Algebraic.MassProduction.Routing.routingPaddingIndex {paddingCount sourceCount destinationCount : ℕ} (padding : Fin paddingCount) : Fin (sourceCount + destinationCount + paddingCount)

Position occupied by a padding record in the semantic routing layout.

Equations

• Algebraic.MassProduction.Routing.routingPaddingIndex padding = Fin.natAdd (sourceCount + destinationCount) padding

@[simp]

theorem Algebraic.MassProduction.Routing.routingRecordSequence_source {sourceCount keyWidth payloadWidth destinationCount paddingCount : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (source : Fin sourceCount) : routingRecordSequence sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads (routingSourceIndex source) = packRecord (sourceKeys source) false (sourcePayloads source)

@[simp]

theorem Algebraic.MassProduction.Routing.routingRecordSequence_destination {sourceCount keyWidth payloadWidth destinationCount paddingCount : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (destination : Fin destinationCount) : routingRecordSequence sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads (routingDestinationIndex destination) = packRecord (destinationKeys destination) true (destinationPayloads destination)

@[simp]

theorem Algebraic.MassProduction.Routing.routingRecordSequence_padding {sourceCount keyWidth payloadWidth destinationCount paddingCount : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (padding : Fin paddingCount) : routingRecordSequence sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads (routingPaddingIndex padding) = packRecord (paddingKeys padding) true (paddingPayloads padding)

def Algebraic.MassProduction.Routing.networkRoutingRecords {sourceCount keyWidth payloadWidth destinationCount paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) : Fin (Sorting.networkRecords depth) → Fin (recordWidth keyWidth payloadWidth) → Bool

Reindex an exactly padded semantic routing layout to the power-of-two record count consumed by the sorting network.

Equations

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

def Algebraic.MassProduction.Routing.networkRoutingSourceIndex {sourceCount destinationCount paddingCount depth : ℕ} (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) (source : Fin sourceCount) : Fin (Sorting.networkRecords depth)

The source's position after the exact-capacity cast.

Equations

• Algebraic.MassProduction.Routing.networkRoutingSourceIndex recordCount source = Fin.cast recordCount (Algebraic.MassProduction.Routing.routingSourceIndex source)

def Algebraic.MassProduction.Routing.networkRoutingDestinationIndex {sourceCount destinationCount paddingCount depth : ℕ} (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) (destination : Fin destinationCount) : Fin (Sorting.networkRecords depth)

The destination's position after the exact-capacity cast.

Equations

• Algebraic.MassProduction.Routing.networkRoutingDestinationIndex recordCount destination = Fin.cast recordCount (Algebraic.MassProduction.Routing.routingDestinationIndex destination)

def Algebraic.MassProduction.Routing.networkRoutingPaddingIndex {sourceCount destinationCount paddingCount depth : ℕ} (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) (padding : Fin paddingCount) : Fin (Sorting.networkRecords depth)

The padding record's position after the exact-capacity cast.

Equations

• Algebraic.MassProduction.Routing.networkRoutingPaddingIndex recordCount padding = Fin.cast recordCount (Algebraic.MassProduction.Routing.routingPaddingIndex padding)

@[simp]

theorem Algebraic.MassProduction.Routing.networkRoutingRecords_source {sourceCount keyWidth payloadWidth destinationCount paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) (source : Fin sourceCount) : networkRoutingRecords sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads recordCount (networkRoutingSourceIndex recordCount source) = packRecord (sourceKeys source) false (sourcePayloads source)

@[simp]

theorem Algebraic.MassProduction.Routing.networkRoutingRecords_destination {sourceCount keyWidth payloadWidth destinationCount paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) (destination : Fin destinationCount) : networkRoutingRecords sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads recordCount (networkRoutingDestinationIndex recordCount destination) = packRecord (destinationKeys destination) true (destinationPayloads destination)

@[simp]

theorem Algebraic.MassProduction.Routing.networkRoutingRecords_padding {sourceCount keyWidth payloadWidth destinationCount paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) (padding : Fin paddingCount) : networkRoutingRecords sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads recordCount (networkRoutingPaddingIndex recordCount padding) = packRecord (paddingKeys padding) true (paddingPayloads padding)

Flattening semantic records into sorter input wires

def Algebraic.MassProduction.Routing.recordArrayBits {depth packedWidth : ℕ} (records : Fin (Sorting.networkRecords depth) → Fin packedWidth → Bool) : Fin (Sorting.networkBits depth packedWidth) → Bool

Row-major bit packing of an already constructed record sequence.

Equations

• Algebraic.MassProduction.Routing.recordArrayBits records flat = records (finProdFinEquiv.symm flat).1 (finProdFinEquiv.symm flat).2

@[simp]

theorem Algebraic.MassProduction.Routing.flatRecords_recordArrayBits {depth packedWidth : ℕ} (records : Fin (Sorting.networkRecords depth) → Fin packedWidth → Bool) : Sorting.flatRecords (recordArrayBits records) = records

Flattening and then reading by records is an exact round trip.

def Algebraic.MassProduction.Routing.routingInputBits {sourceCount keyWidth payloadWidth destinationCount paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) : Fin (Sorting.networkBits depth (recordWidth keyWidth payloadWidth)) → Bool

Fully packed bit input for one exactly padded routing network.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Routing.flatRecords_routingInputBits {sourceCount keyWidth payloadWidth destinationCount paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) : Sorting.flatRecords (routingInputBits sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads recordCount) = networkRoutingRecords sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads recordCount

theorem Algebraic.MassProduction.Routing.routingInputBits_unique_destination {sourceCount keyWidth payloadWidth destinationCount paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (destinationKeysInjective : Function.Injective destinationKeys) (paddingAvoidsDestination : ∀ (padding : Fin paddingCount) (destination : Fin destinationCount), paddingKeys padding ≠ destinationKeys destination) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) (destination : Fin destinationCount) : have input := routingInputBits sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads recordCount; UniqueIndexWhere (Sorting.flatRecords input) (recordHasKeyTag (destinationKeys destination) true)

Every packed destination remains uniquely identifiable after exact capacity padding and flattening, even when no source uses its key.

theorem Algebraic.MassProduction.Routing.routingInputBits_unique_source {sourceCount keyWidth payloadWidth destinationCount paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (sourceKeysInjective : Function.Injective sourceKeys) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) (source : Fin sourceCount) : have input := routingInputBits sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads recordCount; UniqueIndexWhere (Sorting.flatRecords input) (recordHasKeyTag (sourceKeys source) false)

Exact-capacity packing retains uniqueness of every source record.

theorem Algebraic.MassProduction.Routing.routingInputBits_unique_key {sourceCount keyWidth payloadWidth destinationCount paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (sourceKeysInjective : Function.Injective sourceKeys) (destinationKeysInjective : Function.Injective destinationKeys) (destinationFor : Fin sourceCount → Fin destinationCount) (destinationKey : ∀ (source : Fin sourceCount), destinationKeys (destinationFor source) = sourceKeys source) (paddingAvoids : ∀ (padding : Fin paddingCount) (source : Fin sourceCount), paddingKeys padding ≠ sourceKeys source) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) (source : Fin sourceCount) : have input := routingInputBits sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads recordCount; UniqueIndexWhere (Sorting.flatRecords input) (recordHasKeyTag (sourceKeys source) false) ∧ UniqueIndexWhere (Sorting.flatRecords input) (recordHasKeyTag (sourceKeys source) true)

The packed sorter input retains the unique source/destination invariant proved for the semantic record layout.

theorem Algebraic.MassProduction.Routing.routingInputBits_routes_source_payload {sourceCount keyWidth payloadWidth destinationCount paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationPayloads : Fin destinationCount → Fin payloadWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (sourceKeysInjective : Function.Injective sourceKeys) (destinationKeysInjective : Function.Injective destinationKeys) (destinationFor : Fin sourceCount → Fin destinationCount) (destinationKey : ∀ (source : Fin sourceCount), destinationKeys (destinationFor source) = sourceKeys source) (paddingAvoids : ∀ (padding : Fin paddingCount) (source : Fin sourceCount), paddingKeys padding ≠ sourceKeys source) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) (source : Fin sourceCount) : have input := routingInputBits sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads recordCount; have sorted := Sorting.bitonicSortBits ⋯ depth true input; ∃ (destinationSorted : Fin (Sorting.networkRecords depth)), recordHasKeyTag (sourceKeys source) true (Sorting.flatRecords sorted destinationSorted) ∧ recordPayload ((sortedPredecessorCopyCircuit depth keyWidth payloadWidth false true).eval DeMorgan.interpretation input) destinationSorted = sourcePayloads source

End-to-end scatter correctness for the concrete record layout. For every active source, the actual sorting-and-predecessor-copy circuit produces the source payload at the uniquely keyed destination record.