Batched OR lookup without source uniqueness

The same shared broadcast router can aggregate Boolean source flags. A destination receives true exactly when some same-key source is true. This allows repeated occupied-point descriptions and returns false for points that are absent from the occupied set.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.sortedCircuit_valueOr {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (header : Lex (Fin (metadataWidth + 1) → Bool)) (key : Fin keyWidth → Bool) (queryCorrect : ∀ (record : Fin (Sorting.networkRecords depth)), CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords input record) = header → Routing.recordKey input record = key ∧ Routing.recordTag input record = true) (destination : Fin (Sorting.networkRecords depth)) (destinationHeader : CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords ((sortedCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input) destination) = header) (bit : Fin valueWidth) : RoutingMetadata.recordValue ((sortedCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input) destination bit = true ↔ ∃ (source : Fin (Sorting.networkRecords depth)), Routing.recordKey input source = key ∧ Routing.recordTag input source = false ∧ RoutingMetadata.recordValue input source bit = true

Broadcast OR correctness before the final ordering pass.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.routingCircuit_fixedOr {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (header : Lex (Fin (metadataWidth + 1) → Bool)) (target : Fin (Sorting.networkRecords depth)) (key : Fin keyWidth → Bool) (uniqueHeader : Sorting.Semantics.UniqueIndexWhere (fun (record : Fin (Sorting.networkRecords depth)) => CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords input record)) fun (candidate : Lex (Fin (metadataWidth + 1) → Bool)) => candidate = header) (rank : (Sorting.Semantics.matchingIndices (fun (record : Fin (Sorting.networkRecords depth)) => CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords input record)) fun (candidate : Lex (Fin (metadataWidth + 1) → Bool)) => candidate < header).card = ↑target) (queryCorrect : ∀ (record : Fin (Sorting.networkRecords depth)), CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords input record) = header → Routing.recordKey input record = key ∧ Routing.recordTag input record = true) (bit : Fin valueWidth) : RoutingMetadata.recordValue ((routingCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input) target bit = true ↔ ∃ (source : Fin (Sorting.networkRecords depth)), Routing.recordKey input source = key ∧ Routing.recordTag input source = false ∧ RoutingMetadata.recordValue input source bit = true

A fixed output position receives the OR of every same-key source bit. No source uniqueness or existence premise is needed.