Identifying source records without key uniqueness

In the packed routing layout, the false tag identifies exactly the source prefix. Source keys and payloads may repeat arbitrarily.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.routingRecordSequence_sourceOfTag {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) (index : Fin (sourceCount + destinationCount + paddingCount)) (sourceTag : Routing.packedRecordTag (Routing.routingRecordSequence sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads index) = false) : ∃ (source : Fin sourceCount), Routing.routingRecordSequence sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads index = Routing.packRecord (sourceKeys source) false (sourcePayloads source)

Every false-tagged raw routing record is one of the declared sources.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.routingInputBits_sourceOfTag {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) (index : Fin (Sorting.networkRecords depth)) (sourceTag : Routing.recordTag (Routing.routingInputBits sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads recordCount) index = false) : ∃ (source : Fin sourceCount), Sorting.flatRecords (Routing.routingInputBits sourceKeys sourcePayloads destinationKeys destinationPayloads paddingKeys paddingPayloads recordCount) index = Routing.packRecord (sourceKeys source) false (sourcePayloads source)

The same source classification holds after casting and flattening to the exact power-of-two routing capacity.