Broadcast correctness with repeated destinations

Sorting a unique source before all same-key destinations creates one linked run. The shared propagation circuit carries its payload to every destination in that run. The number of destinations is unrestricted.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.payloadCircuit_eq_true_iff {payloadWidth depth keyWidth : ℕ} (bit : Fin payloadWidth) (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (record : Fin (Sorting.networkRecords depth)) : (payloadCircuit depth keyWidth payloadWidth bit).eval DeMorgan.interpretation input record = true ↔ ∃ start ≤ record, Routing.recordTag input start = false ∧ Routing.recordPayload input start bit = true ∧ ∀ (index : Fin (Sorting.networkRecords depth)), start < index → index ≤ record → DeMorgan.Expression.eval input (linkExpression depth keyWidth payloadWidth index) = true

The concrete broadcast bit has a source connected by adjacent links.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.sameKeyOfLinked {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (start finish : Fin (Sorting.networkRecords depth)) (ordered : start ≤ finish) (links : ∀ (index : Fin (Sorting.networkRecords depth)), start < index → index ≤ finish → DeMorgan.Expression.eval input (linkExpression depth keyWidth payloadWidth index) = true) : Routing.recordKey input start = Routing.recordKey input finish

Adjacent links force the key at the source and destination to agree.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.payloadCircuit_routesInterval {payloadWidth depth keyWidth : ℕ} (bit : Fin payloadWidth) (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (source destination : Fin (Sorting.networkRecords depth)) (ordered : source ≤ destination) (sourceTag : Routing.recordTag input source = false) (sourceUnique : ∀ (index : Fin (Sorting.networkRecords depth)), Routing.recordKey input index = Routing.recordKey input source → Routing.recordTag input index = false → index = source) (interval : ∀ (index : Fin (Sorting.networkRecords depth)), source ≤ index → index ≤ destination → Routing.recordKey input index = Routing.recordKey input source) : (payloadCircuit depth keyWidth payloadWidth bit).eval DeMorgan.interpretation input destination = Routing.recordPayload input source bit

A unique source supplies every record in its linked interval. Only the source is required to be unique; repeated destinations are permitted.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.sourceIntervalOfSorted {depth keyWidth payloadWidth : ℕ} (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (source destination : Fin (Sorting.networkRecords depth)) (sameKey : Routing.recordKey input source = Routing.recordKey input destination) (sourceTag : Routing.recordTag input source = false) (destinationTag : Routing.recordTag input destination = true) : source ≤ destination ∧ ∀ (index : Fin (Sorting.networkRecords depth)), source ≤ index → index ≤ destination → Routing.recordKey input index = Routing.recordKey input source

In a sorted array, the source and every same-key destination enclose only records having that key. This follows from the covered tag pair.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.payloadCircuit_routesSorted {payloadWidth depth keyWidth : ℕ} (bit : Fin payloadWidth) (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (source destination : Fin (Sorting.networkRecords depth)) (sameKey : Routing.recordKey input source = Routing.recordKey input destination) (sourceTag : Routing.recordTag input source = false) (destinationTag : Routing.recordTag input destination = true) (sourceUnique : ∀ (index : Fin (Sorting.networkRecords depth)), Routing.recordKey input index = Routing.recordKey input source → Routing.recordTag input index = false → index = source) : (payloadCircuit depth keyWidth payloadWidth bit).eval DeMorgan.interpretation input destination = Routing.recordPayload input source bit

Sorted broadcasting routes one unique source to any same-key destination. No uniqueness premise is imposed on destination keys.

theorem Algebraic.MassProduction.Nonuniform.Broadcast.payloadCircuit_routesSorted_iff {payloadWidth depth keyWidth : ℕ} (bit : Fin payloadWidth) (input : Fin (Sorting.networkBits depth (Routing.recordWidth keyWidth payloadWidth)) → Bool) (sorted : Sorting.FlatKeysSorted ⋯ true input) (destination : Fin (Sorting.networkRecords depth)) (destinationTag : Routing.recordTag input destination = true) : (payloadCircuit depth keyWidth payloadWidth bit).eval DeMorgan.interpretation input destination = true ↔ ∃ (source : Fin (Sorting.networkRecords depth)), Routing.recordKey input source = Routing.recordKey input destination ∧ Routing.recordTag input source = false ∧ Routing.recordPayload input source bit = true

Boolean broadcast computes the OR of every same-key source bit. This form permits repeated source keys and gives false when no source matches.