Canonical ordering by preserved routing metadata

After gather matching, destination records must be ordered by their preserved (request, line position) metadata rather than by the (group, point) key used for matching. This module constructs the free within-record permutation selecting (tag, metadata) as the second sort key, preceded by the same explicit tag-complement pass used for scatter.

def Algebraic.MassProduction.CanonicalMetadataRouting.metadataOrderForward (keyWidth metadataWidth valueWidth : ℕ) (bit : Fin (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) : Fin (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)

Forward block swap taking virtual (tag, metadata, matching key, value) positions to physical (matching key, tag, metadata, value) positions.

Equations

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

def Algebraic.MassProduction.CanonicalMetadataRouting.metadataOrderBackward (keyWidth metadataWidth valueWidth : ℕ) (bit : Fin (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) : Fin (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)

Inverse physical-to-virtual block swap.

Equations

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

def Algebraic.MassProduction.CanonicalMetadataRouting.metadataOrderBitOrder (keyWidth metadataWidth valueWidth : ℕ) : Equiv.Perm (Fin (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth))

Permutation swapping the matching-key and (tag, metadata) blocks while leaving the copied-value block fixed.

Equations

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

theorem Algebraic.MassProduction.CanonicalMetadataRouting.metadataOrderKeyFits (keyWidth metadataWidth valueWidth : ℕ) : metadataWidth + 1 ≤ RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth

theorem Algebraic.MassProduction.CanonicalMetadataRouting.metadataOrderBitOrder_prefix {metadataWidth keyWidth valueWidth : ℕ} (bit : Fin (metadataWidth + 1)) : (metadataOrderBitOrder keyWidth metadataWidth valueWidth) (Fin.castLE ⋯ bit) = ⟨keyWidth + ↑bit, ⋯⟩

A virtual (tag, metadata) bit maps to the corresponding physical bit after the matching-key block.

theorem Algebraic.MassProduction.CanonicalMetadataRouting.metadataOrderVirtualKey {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : Sorting.flatRecordKey ⋯ (Sorting.flatRecords (Sorting.reindexRecordBits (metadataOrderBitOrder keyWidth metadataWidth valueWidth) input) record) = toLex (Fin.cons (Routing.recordTag input record) (RoutingMetadata.recordMetadata input record))

The selected virtual prefix is exactly the complemented physical tag followed by the preserved metadata field.

def Algebraic.MassProduction.CanonicalMetadataRouting.canonicalSortBits (depth keyWidth metadataWidth valueWidth : ℕ) (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool

Flip tags and canonically order complete records by (tag, metadata).

Equations

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

def Algebraic.MassProduction.CanonicalMetadataRouting.canonicalSortCircuit (depth keyWidth metadataWidth valueWidth : ℕ) : Circuit DeMorgan.signature (Sorting.networkBits depth (Routing.recordWidth keyWidth (metadataWidth + valueWidth))) (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth))

Explicit tag-flip and metadata-ordering circuit.

Equations

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

@[simp]

theorem Algebraic.MassProduction.CanonicalMetadataRouting.canonicalSortCircuit_size (depth keyWidth metadataWidth valueWidth : ℕ) : (canonicalSortCircuit depth keyWidth metadataWidth valueWidth).size = ∑ output : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth (metadataWidth + valueWidth))), CanonicalRouting.complementTagOutputGateCount depth keyWidth (metadataWidth + valueWidth) output + Sorting.bitonicSortGateCount ⋯ depth

The exact gate count of canonicalSortCircuit.

@[simp]

theorem Algebraic.MassProduction.CanonicalMetadataRouting.canonicalSortCircuit_eval {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) : (canonicalSortCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input = canonicalSortBits depth keyWidth metadataWidth valueWidth input

theorem Algebraic.MassProduction.CanonicalMetadataRouting.canonicalSortBits_recordsPermute {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) : Sorting.FlatRecordsPermute (canonicalSortBits depth keyWidth metadataWidth valueWidth input) (CanonicalRouting.complementRoutingTagsBits depth keyWidth (metadataWidth + valueWidth) input)

theorem Algebraic.MassProduction.CanonicalMetadataRouting.canonicalSortBits_keysSorted {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) : Sorting.FlatKeysSortedBy (metadataOrderBitOrder keyWidth metadataWidth valueWidth) ⋯ true (canonicalSortBits depth keyWidth metadataWidth valueWidth input)

theorem Algebraic.MassProduction.CanonicalMetadataRouting.canonicalSortCircuit_cost_le {depth keyWidth metadataWidth valueWidth : ℕ} : (canonicalSortCircuit depth keyWidth metadataWidth valueWidth).cost DeMorgan.standardCost ≤ Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth) + depth * depth * Sorting.networkRecords depth * (2 * RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth * (2 * ((metadataWidth + 1) * (6 * (metadataWidth + 1) + 4)) + 4))

Complete gather-match and canonical-order pipeline

def Algebraic.MassProduction.CanonicalMetadataRouting.recordHeader {keyWidth metadataWidth valueWidth : ℕ} (record : Fin (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth) → Bool) : Lex (Fin (metadataWidth + 1) → Bool)

Canonical (tag, metadata) header of a standalone record.

Equations

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

def Algebraic.MassProduction.CanonicalMetadataRouting.complementedRecordHeader {keyWidth metadataWidth valueWidth : ℕ} (record : Fin (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth) → Bool) : Lex (Fin (metadataWidth + 1) → Bool)

Metadata header after complementing the record tag.

Equations

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

@[simp]

theorem Algebraic.MassProduction.CanonicalMetadataRouting.recordMetadata_complementRoutingTagsBits {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : RoutingMetadata.recordMetadata (CanonicalRouting.complementRoutingTagsBits depth keyWidth (metadataWidth + valueWidth) input) record = RoutingMetadata.recordMetadata input record

@[simp]

theorem Algebraic.MassProduction.CanonicalMetadataRouting.recordValue_complementRoutingTagsBits {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : RoutingMetadata.recordValue (CanonicalRouting.complementRoutingTagsBits depth keyWidth (metadataWidth + valueWidth) input) record = RoutingMetadata.recordValue input record

@[simp]

theorem Algebraic.MassProduction.CanonicalMetadataRouting.recordHeader_flatRecords {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : recordHeader (Sorting.flatRecords input record) = toLex (Fin.cons (Routing.recordTag input record) (RoutingMetadata.recordMetadata input record))

theorem Algebraic.MassProduction.CanonicalMetadataRouting.recordHeader_complementRoutingTagsBits {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : recordHeader (Sorting.flatRecords (CanonicalRouting.complementRoutingTagsBits depth keyWidth (metadataWidth + valueWidth) input) record) = complementedRecordHeader (Sorting.flatRecords input record)

theorem Algebraic.MassProduction.CanonicalMetadataRouting.recordHeader_predecessorCopyBits {depth keyWidth metadataWidth valueWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : recordHeader (Sorting.flatRecords (RoutingMetadata.predecessorCopyBits depth keyWidth metadataWidth valueWidth sourceTag destinationTag input) record) = recordHeader (Sorting.flatRecords input record)

@[simp]

theorem Algebraic.MassProduction.CanonicalMetadataRouting.complementedRecordHeader_predecessorCopyBits {depth keyWidth metadataWidth valueWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : complementedRecordHeader (Sorting.flatRecords (RoutingMetadata.predecessorCopyBits depth keyWidth metadataWidth valueWidth sourceTag destinationTag input) record) = complementedRecordHeader (Sorting.flatRecords input record)

def Algebraic.MassProduction.CanonicalMetadataRouting.matchedCanonicalRoutingBits (depth keyWidth metadataWidth valueWidth : ℕ) (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool

Semantic gather match followed by canonical metadata ordering.

Equations

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

def Algebraic.MassProduction.CanonicalMetadataRouting.matchedCanonicalRoutingCircuit (depth keyWidth metadataWidth valueWidth : ℕ) : Circuit DeMorgan.signature (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth))

Explicit two-sort gather circuit.

Equations

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

@[simp]

theorem Algebraic.MassProduction.CanonicalMetadataRouting.matchedCanonicalRoutingCircuit_size (depth keyWidth metadataWidth valueWidth : ℕ) : (matchedCanonicalRoutingCircuit depth keyWidth metadataWidth valueWidth).size = RoutingMetadata.sortedPredecessorCopyGateCount depth keyWidth metadataWidth valueWidth false true + (canonicalSortCircuit depth keyWidth metadataWidth valueWidth).size

The exact gate count of matchedCanonicalRoutingCircuit.

@[simp]

theorem Algebraic.MassProduction.CanonicalMetadataRouting.matchedCanonicalRoutingCircuit_eval {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) : (matchedCanonicalRoutingCircuit depth keyWidth metadataWidth valueWidth).eval DeMorgan.interpretation input = matchedCanonicalRoutingBits depth keyWidth metadataWidth valueWidth input

theorem Algebraic.MassProduction.CanonicalMetadataRouting.matchedCanonicalRoutingCircuit_cost_le {depth keyWidth metadataWidth valueWidth : ℕ} : (matchedCanonicalRoutingCircuit depth keyWidth metadataWidth valueWidth).cost DeMorgan.standardCost ≤ depth * depth * Sorting.networkRecords depth * (2 * RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth * (2 * ((keyWidth + 1) * (6 * (keyWidth + 1) + 4)) + 4)) + Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth) * (12 * keyWidth + 12) + (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth) + depth * depth * Sorting.networkRecords depth * (2 * RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth * (2 * ((metadataWidth + 1) * (6 * (metadataWidth + 1) + 4)) + 4)))

theorem Algebraic.MassProduction.CanonicalMetadataRouting.matchedCanonicalHeadersPermute {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) : have initiallySorted := Sorting.bitonicSortBits ⋯ depth true input; have routed := RoutingMetadata.predecessorCopyBits depth keyWidth metadataWidth valueWidth false true initiallySorted; have output := canonicalSortBits depth keyWidth metadataWidth valueWidth routed; Sorting.Semantics.SequencePermutes (fun (record : Fin (Sorting.networkRecords depth)) => recordHeader (Sorting.flatRecords output record)) fun (record : Fin (Sorting.networkRecords depth)) => complementedRecordHeader (Sorting.flatRecords input record)

The complete metadata-routing pipeline permutes complemented initial (tag, metadata) headers.

Canonical rank of destination metadata

noncomputable def Algebraic.MassProduction.CanonicalMetadataRouting.destinationOrderMetadata {destinationCount orderWidth : ℕ} (destinationFits : destinationCount ≤ 2 ^ orderWidth) (destination : Fin destinationCount) : Fin (orderWidth + 1) → Bool

Destination metadata at one canonical prefix position.

Equations

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

@[simp]

theorem Algebraic.MassProduction.CanonicalMetadataRouting.complementedRecordHeader_packRecord {keyWidth metadataWidth valueWidth : ℕ} (key : Fin keyWidth → Bool) (tag : Bool) (metadata : Fin metadataWidth → Bool) (value : Fin valueWidth → Bool) : complementedRecordHeader (RoutingMetadata.packRecord key tag metadata value) = toLex (Fin.cons (!tag) metadata)

theorem Algebraic.MassProduction.CanonicalMetadataRouting.destinationHeader_injective {orderWidth : ℕ} : Function.Injective CanonicalRouting.activeDestinationHeader

theorem Algebraic.MassProduction.CanonicalMetadataRouting.complementedSourceHeader_not_lt_destination {keyWidth orderWidth valueWidth : ℕ} (key : Fin keyWidth → Bool) (metadata : Fin (orderWidth + 1) → Bool) (value : Fin valueWidth → Bool) (target : Fin orderWidth → Bool) : ¬complementedRecordHeader (RoutingMetadata.packRecord key false metadata value) < CanonicalRouting.activeDestinationHeader target

theorem Algebraic.MassProduction.CanonicalMetadataRouting.complementedPaddingHeader_not_lt_destination {keyWidth orderWidth valueWidth : ℕ} (key : Fin keyWidth → Bool) (paddingTail : Fin orderWidth → Bool) (value : Fin valueWidth → Bool) (target : Fin orderWidth → Bool) : ¬complementedRecordHeader (RoutingMetadata.packRecord key true (paddingRoutingKey paddingTail) value) < CanonicalRouting.activeDestinationHeader target

theorem Algebraic.MassProduction.CanonicalMetadataRouting.complementedDestinationHeader_lt_iff {keyWidth orderWidth valueWidth : ℕ} (key : Fin keyWidth → Bool) (left right : Fin orderWidth → Bool) (value : Fin valueWidth → Bool) : complementedRecordHeader (RoutingMetadata.packRecord key true (activeRoutingKey left) value) < CanonicalRouting.activeDestinationHeader right ↔ toLex left < toLex right

theorem Algebraic.MassProduction.CanonicalMetadataRouting.routingRecordSequence_orderHeader_count_lt {destinationCount orderWidth sourceCount keyWidth valueWidth paddingCount : ℕ} (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) (target : Fin destinationCount) : (Sorting.Semantics.matchingIndices (fun (record : Fin (sourceCount + destinationCount + paddingCount)) => complementedRecordHeader (Routing.routingRecordSequence sourceKeys (fun (source : Fin sourceCount) => Fin.append (sourceMetadata source) (sourceValues source)) destinationKeys (fun (destination : Fin destinationCount) => Fin.append (destinationOrderMetadata destinationFits destination) (destinationValues destination)) paddingKeys (fun (padding : Fin paddingCount) => Fin.append (paddingRoutingKey (paddingTails padding)) (paddingValues padding)) record)) fun (header : Lex (Fin (orderWidth + 1 + 1) → Bool)) => header < CanonicalRouting.activeDestinationHeader (lexBitVectorAt (Fin.castLE destinationFits target))).card = ↑target

Exactly target.val initial records have complemented order metadata strictly below the target destination's canonical metadata.

theorem Algebraic.MassProduction.CanonicalMetadataRouting.routingInputBits_orderHeader_count_lt {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) : have input := Routing.routingInputBits sourceKeys (fun (source : Fin sourceCount) => Fin.append (sourceMetadata source) (sourceValues source)) destinationKeys (fun (destination : Fin destinationCount) => Fin.append (destinationOrderMetadata destinationFits destination) (destinationValues destination)) paddingKeys (fun (padding : Fin paddingCount) => Fin.append (paddingRoutingKey (paddingTails padding)) (paddingValues padding)) recordCount; (Sorting.Semantics.matchingIndices (fun (record : Fin (Sorting.networkRecords depth)) => complementedRecordHeader (Sorting.flatRecords input record)) fun (header : Lex (Fin (orderWidth + 1 + 1) → Bool)) => header < CanonicalRouting.activeDestinationHeader (lexBitVectorAt (Fin.castLE destinationFits target))).card = ↑target

Flattening and exact-capacity casting preserve the destination metadata rank count.

Unique canonical destination headers

theorem Algebraic.MassProduction.CanonicalMetadataRouting.complementedRecordHeader_eq_activeDestinationHeader_iff {keyWidth orderWidth valueWidth : ℕ} (record : Fin (RoutingMetadata.recordWidth keyWidth (orderWidth + 1) valueWidth) → Bool) (target : Fin orderWidth → Bool) : complementedRecordHeader record = CanonicalRouting.activeDestinationHeader target ↔ Routing.packedRecordTag record = true ∧ RoutingMetadata.packedRecordMetadata record = activeRoutingKey target

theorem Algebraic.MassProduction.CanonicalMetadataRouting.routingRecordSequence_unique_order_header {destinationCount orderWidth sourceCount keyWidth valueWidth paddingCount : ℕ} (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) (target : Fin destinationCount) : Sorting.Semantics.UniqueIndexWhere (Routing.routingRecordSequence sourceKeys (fun (source : Fin sourceCount) => Fin.append (sourceMetadata source) (sourceValues source)) destinationKeys (fun (destination : Fin destinationCount) => Fin.append (destinationOrderMetadata destinationFits destination) (destinationValues destination)) paddingKeys fun (padding : Fin paddingCount) => Fin.append (paddingRoutingKey (paddingTails padding)) (paddingValues padding)) fun (record : Fin (Routing.recordWidth keyWidth (orderWidth + 1 + valueWidth)) → Bool) => complementedRecordHeader record = CanonicalRouting.activeDestinationHeader (lexBitVectorAt (Fin.castLE destinationFits target))

The canonical metadata header for one destination occurs exactly once in the semantic routing layout. Matching keys need not be injective here: the preserved destination-order metadata supplies the uniqueness.

theorem Algebraic.MassProduction.CanonicalMetadataRouting.routingInputBits_unique_order_header {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) : have input := Routing.routingInputBits sourceKeys (fun (source : Fin sourceCount) => Fin.append (sourceMetadata source) (sourceValues source)) destinationKeys (fun (destination : Fin destinationCount) => Fin.append (destinationOrderMetadata destinationFits destination) (destinationValues destination)) paddingKeys (fun (padding : Fin paddingCount) => Fin.append (paddingRoutingKey (paddingTails padding)) (paddingValues padding)) recordCount; Sorting.Semantics.UniqueIndexWhere (Sorting.flatRecords input) fun (record : Fin (Routing.recordWidth keyWidth (orderWidth + 1 + valueWidth)) → Bool) => complementedRecordHeader record = CanonicalRouting.activeDestinationHeader (lexBitVectorAt (Fin.castLE destinationFits target))

Exact-capacity casting and flattening retain the unique canonical destination metadata header.

Fixed output positions

theorem Algebraic.MassProduction.CanonicalMetadataRouting.matchedCanonicalRoutingBits_fixed_header {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) : have input := Routing.routingInputBits sourceKeys (fun (source : Fin sourceCount) => Fin.append (sourceMetadata source) (sourceValues source)) destinationKeys (fun (destination : Fin destinationCount) => Fin.append (destinationOrderMetadata destinationFits destination) (destinationValues destination)) paddingKeys (fun (padding : Fin paddingCount) => Fin.append (paddingRoutingKey (paddingTails padding)) (paddingValues padding)) recordCount; have output := matchedCanonicalRoutingBits depth keyWidth (orderWidth + 1) valueWidth input; have destinationFitsNetwork := ⋯; recordHeader (Sorting.flatRecords output (Fin.castLE destinationFitsNetwork target)) = CanonicalRouting.activeDestinationHeader (lexBitVectorAt (Fin.castLE destinationFits target))

After matching by the runtime key and sorting by preserved destination metadata, destination target occupies literal output record target.

theorem Algebraic.MassProduction.CanonicalMetadataRouting.matchedCanonicalRoutingBits_fixed_value {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) (sourceKeysInjective : Function.Injective sourceKeys) (destinationKeysInjective : Function.Injective destinationKeys) (sourceFor : Fin destinationCount → Fin sourceCount) (matchingKey : ∀ (destination : Fin destinationCount), sourceKeys (sourceFor destination) = destinationKeys destination) (paddingAvoids : ∀ (padding : Fin paddingCount) (destination : Fin destinationCount), paddingKeys padding ≠ destinationKeys destination) (recordCount : sourceCount + destinationCount + paddingCount = Sorting.networkRecords depth) (target : Fin destinationCount) : have input := Routing.routingInputBits sourceKeys (fun (source : Fin sourceCount) => Fin.append (sourceMetadata source) (sourceValues source)) destinationKeys (fun (destination : Fin destinationCount) => Fin.append (destinationOrderMetadata destinationFits destination) (destinationValues destination)) paddingKeys (fun (padding : Fin paddingCount) => Fin.append (paddingRoutingKey (paddingTails padding)) (paddingValues padding)) recordCount; have output := matchedCanonicalRoutingBits depth keyWidth (orderWidth + 1) valueWidth input; have destinationFitsNetwork := ⋯; RoutingMetadata.recordValue output (Fin.castLE destinationFitsNetwork target) = sourceValues (sourceFor target)

The value copied into destination target also occupies its literal canonical output record. This is the generic fixed-wire correctness theorem used by the gather pass.