Canonical ordering after shared broadcast

A unique destination header with known rank determines a literal output position after the second sort. This formulation separates ordering from the matching method, so it also applies when destination matching keys repeat.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.canonicalHeadersIncreasing {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) : Sorting.Semantics.SequenceIncreasing fun (record : Fin (Sorting.networkRecords depth)) => CanonicalMetadataRouting.recordHeader (Sorting.flatRecords (CanonicalMetadataRouting.canonicalSortBits depth keyWidth metadataWidth valueWidth input) record)

Canonical sorting produces increasing physical destination headers.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.canonicalHeadersPermute {depth keyWidth metadataWidth valueWidth : ℕ} (input : Fin (Sorting.networkBits depth (RoutingMetadata.recordWidth keyWidth metadataWidth valueWidth)) → Bool) : Sorting.Semantics.SequencePermutes (fun (record : Fin (Sorting.networkRecords depth)) => CanonicalMetadataRouting.recordHeader (Sorting.flatRecords (CanonicalMetadataRouting.canonicalSortBits depth keyWidth metadataWidth valueWidth input) record)) fun (record : Fin (Sorting.networkRecords depth)) => CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords input record)

Canonical sorting permutes exactly the complemented initial headers.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.canonicalSort_fixedValue {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)) (value : Fin valueWidth → Bool) (unique : 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) (valueCorrect : ∀ (record : Fin (Sorting.networkRecords depth)), CanonicalMetadataRouting.complementedRecordHeader (Sorting.flatRecords input record) = header → RoutingMetadata.recordValue input record = value) : RoutingMetadata.recordValue (CanonicalMetadataRouting.canonicalSortBits depth keyWidth metadataWidth valueWidth input) target = value

A unique header with known rank sends its associated value to a fixed output wire. No restriction is imposed on its earlier matching key.