Canonical fixed-wire routing layouts

The matching pass identifies a destination by data-dependent sorted position. Resource circuits, however, need one fixed wire for every (group, point) slot. This module adds the second routing sort used in the manuscript:

1. complement every source/destination tag after predecessor copying;
2. reinterpret a record's prefix as (tag, key) rather than (key, tag);
3. sort again in ascending order.

For a full active-key-space destination array, active destinations then form the initial block, in canonical lexicographic key order. All transformations are explicit De Morgan circuits or free wire permutations.

Complementing the physical tag field

def Algebraic.MassProduction.CanonicalRouting.complementTagOutputExpression (depth keyWidth payloadWidth : ℕ) (output : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth))) : DeMorgan.Expression (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth))

One output formula for the tag-complement pass.

Equations

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

def Algebraic.MassProduction.CanonicalRouting.complementRoutingTagsBits (depth keyWidth payloadWidth : ℕ) (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool

Semantic tag complement on a packed routing array.

Equations

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

@[reducible]

def Algebraic.MassProduction.CanonicalRouting.complementTagOutputGateCount (depth keyWidth payloadWidth : ℕ) (output : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth))) : ℕ

Gate count of one tag-complement output formula.

Equations

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

def Algebraic.MassProduction.CanonicalRouting.complementRoutingTagsCircuit (depth keyWidth payloadWidth : ℕ) : Circuit DeMorgan.signature (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth))

Explicit circuit complementing precisely the tag bit of every record.

Equations

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

@[simp]

theorem Algebraic.MassProduction.CanonicalRouting.complementRoutingTagsCircuit_size (depth keyWidth payloadWidth : ℕ) : (complementRoutingTagsCircuit depth keyWidth payloadWidth).size = ∑ output : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)), complementTagOutputGateCount depth keyWidth payloadWidth output

@[simp]

theorem Algebraic.MassProduction.CanonicalRouting.complementRoutingTagsCircuit_eval {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) : (complementRoutingTagsCircuit depth keyWidth payloadWidth).eval DeMorgan.interpretation input = complementRoutingTagsBits depth keyWidth payloadWidth input

@[simp]

theorem Algebraic.MassProduction.CanonicalRouting.complementRoutingTagsBits_recordKey {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : Routing.recordKey (complementRoutingTagsBits depth keyWidth payloadWidth input) record = Routing.recordKey input record

@[simp]

theorem Algebraic.MassProduction.CanonicalRouting.complementRoutingTagsBits_recordTag {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : Routing.recordTag (complementRoutingTagsBits depth keyWidth payloadWidth input) record = !Routing.recordTag input record

@[simp]

theorem Algebraic.MassProduction.CanonicalRouting.complementRoutingTagsBits_recordPayload {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : Routing.recordPayload (complementRoutingTagsBits depth keyWidth payloadWidth input) record = Routing.recordPayload input record

theorem Algebraic.MassProduction.CanonicalRouting.complementTagOutputExpression_standardCost_le {depth keyWidth payloadWidth : ℕ} (output : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth))) : (complementTagOutputExpression depth keyWidth payloadWidth output).standardCost ≤ 1

theorem Algebraic.MassProduction.CanonicalRouting.complementRoutingTagsCircuit_cost_le {depth keyWidth payloadWidth : ℕ} : (complementRoutingTagsCircuit depth keyWidth payloadWidth).cost DeMorgan.standardCost ≤ Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)

The tag complement costs at most one gate per physical input bit (and in fact exactly one gate per record).

Sorting by (tag, key)

def Algebraic.MassProduction.CanonicalRouting.tagFirstBitOrder (keyWidth payloadWidth : ℕ) : Equiv.Perm (Fin (Routing.recordWidth keyWidth payloadWidth))

Within-record permutation taking the virtual order (tag, key, payload) to the physical order (key, tag, payload).

Equations

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

theorem Algebraic.MassProduction.CanonicalRouting.tagFirstVirtualKey {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : Sorting.flatRecordKey ⋯ (Sorting.flatRecords (Sorting.reindexRecordBits (tagFirstBitOrder keyWidth payloadWidth) input) record) = toLex (Fin.cons (Routing.recordTag input record) (Routing.recordKey input record))

The selected virtual prefix is exactly the physical tag followed by the physical routing key.

def Algebraic.MassProduction.CanonicalRouting.canonicalSortBits (depth keyWidth payloadWidth : ℕ) (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool

The complete canonicalization pass: flip tags, then sort by (tag, key). The matching/copy pass is supplied separately so this primitive is reusable for both scatter and gather.

Equations

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

def Algebraic.MassProduction.CanonicalRouting.canonicalSortCircuit (depth keyWidth payloadWidth : ℕ) : Circuit DeMorgan.signature (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth))

Explicit tag-flip and canonical-sort circuit.

Equations

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

@[simp]

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

The exact gate count of canonicalSortCircuit.

@[simp]

theorem Algebraic.MassProduction.CanonicalRouting.canonicalSortCircuit_eval {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) : (canonicalSortCircuit depth keyWidth payloadWidth).eval DeMorgan.interpretation input = canonicalSortBits depth keyWidth payloadWidth input

theorem Algebraic.MassProduction.CanonicalRouting.canonicalSortBits_recordsPermute {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) : Sorting.FlatRecordsPermute (canonicalSortBits depth keyWidth payloadWidth input) (complementRoutingTagsBits depth keyWidth payloadWidth input)

theorem Algebraic.MassProduction.CanonicalRouting.canonicalSortBits_keysSorted {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) : Sorting.FlatKeysSortedBy (tagFirstBitOrder keyWidth payloadWidth) ⋯ true (canonicalSortBits depth keyWidth payloadWidth input)

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

Header permutations through the two routing sorts

def Algebraic.MassProduction.CanonicalRouting.recordHeader {keyWidth payloadWidth : ℕ} (record : Fin (Routing.recordWidth keyWidth payloadWidth) → Bool) : Lex (Fin (keyWidth + 1) → Bool)

Canonical header of a standalone physical routing record.

Equations

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

def Algebraic.MassProduction.CanonicalRouting.complementedRecordHeader {keyWidth payloadWidth : ℕ} (record : Fin (Routing.recordWidth keyWidth payloadWidth) → Bool) : Lex (Fin (keyWidth + 1) → Bool)

Header obtained after complementing the tag of a standalone record.

Equations

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

def Algebraic.MassProduction.CanonicalRouting.activeDestinationHeader {baseWidth : ℕ} (baseKey : Fin baseWidth → Bool) : Lex (Fin (baseWidth + 2) → Bool)

Canonical header occupied by the active destination for one unmarked base key.

Equations

• Algebraic.MassProduction.CanonicalRouting.activeDestinationHeader baseKey = toLex (Fin.cons false (Algebraic.MassProduction.activeRoutingKey baseKey))

@[simp]

theorem Algebraic.MassProduction.CanonicalRouting.complementedRecordHeader_packRecord {keyWidth payloadWidth : ℕ} (key : Fin keyWidth → Bool) (tag : Bool) (payload : Fin payloadWidth → Bool) : complementedRecordHeader (Routing.packRecord key tag payload) = toLex (Fin.cons (!tag) key)

theorem Algebraic.MassProduction.CanonicalRouting.activeDestinationHeader_lt_iff {baseWidth : ℕ} (left right : Fin baseWidth → Bool) : activeDestinationHeader left < activeDestinationHeader right ↔ toLex left < toLex right

theorem Algebraic.MassProduction.CanonicalRouting.complementedSourceHeader_not_lt_active {baseWidth payloadWidth : ℕ} (sourceKey : Fin (baseWidth + 1) → Bool) (sourcePayload : Fin payloadWidth → Bool) (target : Fin baseWidth → Bool) : ¬complementedRecordHeader (Routing.packRecord sourceKey false sourcePayload) < activeDestinationHeader target

theorem Algebraic.MassProduction.CanonicalRouting.complementedPaddingHeader_not_lt_active {baseWidth payloadWidth : ℕ} (paddingTail : Fin baseWidth → Bool) (paddingPayload : Fin payloadWidth → Bool) (target : Fin baseWidth → Bool) : ¬complementedRecordHeader (Routing.packRecord (paddingRoutingKey paddingTail) true paddingPayload) < activeDestinationHeader target

theorem Algebraic.MassProduction.CanonicalRouting.complementedActiveDestinationHeader_lt_iff {baseWidth payloadWidth : ℕ} (left right : Fin baseWidth → Bool) (payload : Fin payloadWidth → Bool) : complementedRecordHeader (Routing.packRecord (activeRoutingKey left) true payload) < activeDestinationHeader right ↔ toLex left < toLex right

@[simp]

theorem Algebraic.MassProduction.CanonicalRouting.recordHeader_flatRecords {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : recordHeader (Sorting.flatRecords input record) = toLex (Fin.cons (Routing.recordTag input record) (Routing.recordKey input record))

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

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

theorem Algebraic.MassProduction.CanonicalRouting.matchingIndices_card_eq_of_sequencePermutes {n : ℕ} {α : Type u_1} {output input : Fin n → α} (predicate : α → Prop) (permuted : Sorting.Semantics.SequencePermutes output input) : (Sorting.Semantics.matchingIndices output predicate).card = (Sorting.Semantics.matchingIndices input predicate).card

Canonical-routing compatibility theorem for preservation of matching position counts under a sequence permutation.

theorem Algebraic.MassProduction.CanonicalRouting.matchingIndices_append_card {leftCount rightCount : ℕ} {α : Type u_1} (left : Fin leftCount → α) (right : Fin rightCount → α) (predicate : α → Prop) : (Sorting.Semantics.matchingIndices (Fin.append left right) predicate).card = (Sorting.Semantics.matchingIndices left predicate).card + (Sorting.Semantics.matchingIndices right predicate).card

Canonical-routing compatibility theorem for matching-position counts in an appended sequence.

theorem Algebraic.MassProduction.CanonicalRouting.matchingIndices_cast_card {leftCount : ℕ} {α : Sort u_1} {rightCount : ℕ} (sequence : Fin leftCount → α) (predicate : α → Prop) (countEquality : leftCount = rightCount) : (Sorting.Semantics.matchingIndices (fun (index : Fin rightCount) => sequence (Fin.cast ⋯ index)) predicate).card = (Sorting.Semantics.matchingIndices sequence predicate).card

Canonical-routing compatibility theorem for matching-position counts under an equality-of-lengths reindexing.

theorem Algebraic.MassProduction.CanonicalRouting.matchingIndices_lt_card_eq_index {κ : Type u_1} {n : ℕ} [LinearOrder κ] (sequence : Fin n → κ) (increasing : Sorting.Semantics.SequenceIncreasing sequence) (index : Fin n) (unique : ∀ (other : Fin n), sequence other = sequence index → other = index) : (Sorting.Semantics.matchingIndices sequence fun (value : κ) => value < sequence index).card = ↑index

Canonical-routing compatibility theorem identifying a unique sorted value's index with the number of smaller entries.

Rank of the complete active-destination block

theorem Algebraic.MassProduction.CanonicalRouting.routingRecordSequence_fullDest_header_count_lt {sourceCount baseWidth payloadWidth paddingCount : ℕ} (sourceKeys : Fin sourceCount → Fin (baseWidth + 1) → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationPayloads : Fin (2 ^ baseWidth) → Fin payloadWidth → Bool) (paddingTails : Fin paddingCount → Fin baseWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (target : Fin (2 ^ baseWidth)) : (Sorting.Semantics.matchingIndices (fun (record : Fin (sourceCount + 2 ^ baseWidth + paddingCount)) => complementedRecordHeader (Routing.routingRecordSequence sourceKeys sourcePayloads (fun (destination : Fin (2 ^ baseWidth)) => activeRoutingKey (lexBitVectorAt destination)) destinationPayloads (fun (padding : Fin paddingCount) => paddingRoutingKey (paddingTails padding)) paddingPayloads record)) fun (header : Lex (Fin (baseWidth + 1 + 1) → Bool)) => header < activeDestinationHeader (lexBitVectorAt target)).card = ↑target

In the semantic source/destination/padding layout, exactly target.val complemented headers lie below the active destination at canonical position target. Source tags exclude the source block; the reserved marker excludes the padding block.

theorem Algebraic.MassProduction.CanonicalRouting.routingInputBits_fullDest_header_count_lt {sourceCount baseWidth payloadWidth paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin (baseWidth + 1) → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationPayloads : Fin (2 ^ baseWidth) → Fin payloadWidth → Bool) (paddingTails : Fin paddingCount → Fin baseWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (recordCount : sourceCount + 2 ^ baseWidth + paddingCount = Sorting.networkRecords depth) (target : Fin (2 ^ baseWidth)) : have input := Routing.routingInputBits sourceKeys sourcePayloads (fun (destination : Fin (2 ^ baseWidth)) => activeRoutingKey (lexBitVectorAt destination)) destinationPayloads (fun (padding : Fin paddingCount) => paddingRoutingKey (paddingTails padding)) paddingPayloads recordCount; (Sorting.Semantics.matchingIndices (fun (record : Fin (Sorting.networkRecords depth)) => complementedRecordHeader (Sorting.flatRecords input record)) fun (header : Lex (Fin (baseWidth + 1 + 1) → Bool)) => header < activeDestinationHeader (lexBitVectorAt target)).card = ↑target

The same exact header-rank statement after flattening and casting the semantic layout to the sorting network's power-of-two capacity.

Complete match-and-canonicalize pass

def Algebraic.MassProduction.CanonicalRouting.matchedCanonicalRoutingBits (depth keyWidth payloadWidth : ℕ) (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool

Semantic composition of the first sort-and-copy pass with the canonical tag-flip and second sort.

Equations

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

def Algebraic.MassProduction.CanonicalRouting.matchedCanonicalRoutingCircuit (depth keyWidth payloadWidth : ℕ) : Circuit DeMorgan.signature (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth))

Explicit two-sort routing circuit: match by (key, tag), copy the source payload, flip tags, then sort by (tag, key).

Equations

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

@[simp]

theorem Algebraic.MassProduction.CanonicalRouting.matchedCanonicalRoutingCircuit_size (depth keyWidth payloadWidth : ℕ) : (matchedCanonicalRoutingCircuit depth keyWidth payloadWidth).size = Routing.sortedPredecessorCopyGateCount depth keyWidth payloadWidth false true + (canonicalSortCircuit depth keyWidth payloadWidth).size

The exact gate count of matchedCanonicalRoutingCircuit.

@[simp]

theorem Algebraic.MassProduction.CanonicalRouting.matchedCanonicalRoutingCircuit_eval {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) : (matchedCanonicalRoutingCircuit depth keyWidth payloadWidth).eval DeMorgan.interpretation input = matchedCanonicalRoutingBits depth keyWidth payloadWidth input

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

theorem Algebraic.MassProduction.CanonicalRouting.canonicalMatchedHeadersPermuteCore {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) : have initiallySorted := Sorting.bitonicSortBits ⋯ depth true input; have routed := Routing.predecessorCopyBits depth keyWidth payloadWidth false true initiallySorted; have canonical := canonicalSortBits depth keyWidth payloadWidth routed; Sorting.Semantics.SequencePermutes (fun (record : Fin (Sorting.networkRecords depth)) => recordHeader (Sorting.flatRecords canonical record)) fun (record : Fin (Sorting.networkRecords depth)) => complementedRecordHeader (Sorting.flatRecords input record)

Header-level permutation invariant for the complete matching and canonicalization pipeline.

theorem Algebraic.MassProduction.CanonicalRouting.complementedRecordHeader_eq_activeDestinationHeader_iff {baseWidth payloadWidth : ℕ} (record : Fin (Routing.recordWidth (baseWidth + 1) payloadWidth) → Bool) (baseKey : Fin baseWidth → Bool) : complementedRecordHeader record = activeDestinationHeader baseKey ↔ Routing.recordHasKeyTag (activeRoutingKey baseKey) true record

theorem Algebraic.MassProduction.CanonicalRouting.recordHasKeyTag_predecessorCopyBits_iff {depth keyWidth payloadWidth : ℕ} (sourceTag destinationTag : Bool) (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) (key : Fin keyWidth → Bool) (tag : Bool) : Routing.recordHasKeyTag key tag (Sorting.flatRecords (Routing.predecessorCopyBits depth keyWidth payloadWidth sourceTag destinationTag input) record) ↔ Routing.recordHasKeyTag key tag (Sorting.flatRecords input record)

theorem Algebraic.MassProduction.CanonicalRouting.recordHeader_complement_eq_activeDestinationHeader_iff {depth baseWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth (baseWidth + 1) payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) (baseKey : Fin baseWidth → Bool) : recordHeader (Sorting.flatRecords (complementRoutingTagsBits depth (baseWidth + 1) payloadWidth input) record) = activeDestinationHeader baseKey ↔ Routing.recordHasKeyTag (activeRoutingKey baseKey) true (Sorting.flatRecords input record)

theorem Algebraic.MassProduction.CanonicalRouting.matchedCanonicalRoutingBits_fullDest_fixed_header {sourceCount baseWidth payloadWidth paddingCount depth : ℕ} (sourceKeys : Fin sourceCount → Fin (baseWidth + 1) → Bool) (sourcePayloads : Fin sourceCount → Fin payloadWidth → Bool) (destinationPayloads : Fin (2 ^ baseWidth) → Fin payloadWidth → Bool) (paddingTails : Fin paddingCount → Fin baseWidth → Bool) (paddingPayloads : Fin paddingCount → Fin payloadWidth → Bool) (recordCount : sourceCount + 2 ^ baseWidth + paddingCount = Sorting.networkRecords depth) (target : Fin (2 ^ baseWidth)) : have input := Routing.routingInputBits sourceKeys sourcePayloads (fun (destination : Fin (2 ^ baseWidth)) => activeRoutingKey (lexBitVectorAt destination)) destinationPayloads (fun (padding : Fin paddingCount) => paddingRoutingKey (paddingTails padding)) paddingPayloads recordCount; have output := matchedCanonicalRoutingBits depth (baseWidth + 1) payloadWidth input; have destinationFits := ⋯; recordHeader (Sorting.flatRecords output (Fin.castLE destinationFits target)) = activeDestinationHeader (lexBitVectorAt target)

Complete active-key-space destinations occupy fixed output positions: position target contains exactly the destination with base key lexBitVectorAt target.

theorem Algebraic.MassProduction.CanonicalRouting.canonicalMatchedHeadersPermute {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) : have initiallySorted := Sorting.bitonicSortBits ⋯ depth true input; have routed := Routing.predecessorCopyBits depth keyWidth payloadWidth false true initiallySorted; have canonical := canonicalSortBits depth keyWidth payloadWidth routed; Sorting.Semantics.SequencePermutes (fun (record : Fin (Sorting.networkRecords depth)) => recordHeader (Sorting.flatRecords canonical record)) fun (record : Fin (Sorting.networkRecords depth)) => complementedRecordHeader (Sorting.flatRecords input record)

The complete match, tag-flip, and canonical-sort pipeline permutes the canonical headers of the initial records after tag complementation. Payload updates do not affect this statement.