OR aggregation in the concrete routing layout

Each destination receives the disjunction of all matching source values. Repeated source keys, repeated queries, and absent keys are all allowed.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.routingCircuit_layoutOr {destinationCount orderWidth sourceCount keyWidth valueWidth paddingCount depth : ℕ} (destinationFits : destinationCount ≤ 2 ^ orderWidth) (sourceKeys : Fin sourceCount → Fin keyWidth → Bool) (sourceMetadata : Fin sourceCount → Fin (orderWidth + 1) → Bool) (sourceValues : Fin sourceCount → Fin valueWidth → Bool) (destinationKeys : Fin destinationCount → Fin keyWidth → Bool) (destinationValues : Fin destinationCount → Fin valueWidth → Bool) (paddingKeys : Fin paddingCount → Fin keyWidth → Bool) (paddingTails : Fin paddingCount → Fin orderWidth → Bool) (paddingValues : Fin paddingCount → Fin valueWidth → Bool) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) (target : Fin destinationCount) (bit : Fin valueWidth) : have input := Routing.routingInputBits sourceKeys (fun (source : Fin sourceCount) => Fin.append (sourceMetadata source) (sourceValues source)) destinationKeys (fun (destination : Fin destinationCount) => Fin.append (CanonicalMetadataRouting.destinationOrderMetadata destinationFits destination) (destinationValues destination)) paddingKeys (fun (padding : Fin paddingCount) => Fin.append (paddingRoutingKey (paddingTails padding)) (paddingValues padding)) recordCount; RoutingMetadata.recordValue ((routingCircuit depth keyWidth (orderWidth + 1) valueWidth).eval DeMorgan.interpretation input) (Fin.castLE ⋯ target) bit = true ↔ ∃ (source : Fin sourceCount), sourceKeys source = destinationKeys target ∧ sourceValues source bit = true

The packed router computes a batched Boolean OR, in literal query order.