Broadcasting along sorted keys

Records are sorted lexicographically by key followed by a tag. False-tagged sources therefore precede true-tagged destinations with the same key. Segmented propagation seeds each source's value and carries it through equal-key links. Each destination receives the OR of every matching source; no uniqueness assumption is needed for this characterization.

Main results

• Cslib.BitString.propagate_sorted_tagged_eq_true_iff: the propagated value at a destination is true precisely when a matching source has a true value.

References

• Adapts the sorted-broadcast argument in MassProduction/Nonuniform/BroadcastCorrectness.lean from S. Schlesinger, Boolean circuit mass production formalization.

theorem Cslib.BitString.propagate_sorted_tagged_eq_true_iff {k n d : ℕ} (key : ℕ → BitString k) (tag payload : ℕ → Bool) (hd : d < n) (htag : tag d = true) (sorted : MonotoneOn (fun (i : ℕ) => toLex (Fin.snoc (key i) (tag i))) (Set.Iio n)) : propagate (fun (i : ℕ) => !tag i && payload i) (keyLinks fun (i : ℕ) => toLex (key i)) (d + 1) = true ↔ ∃ s < n, key s = key d ∧ tag s = false ∧ payload s = true

At a destination in key/tag order, propagation is the OR of all matching source values. False tags mark sources and true tags mark destinations. Sources and destinations may repeat, and sortedness is required only within the indicated prefix.