Segmented propagation of Boolean sources

Each position contributes a source bit. A true link carries the previous value forward; a false link starts a new segment. The value of a prefix is true precisely when it contains a true source connected to the end by uninterrupted true links. The link at the source itself is irrelevant, including the first link.

Main definitions

• Cslib.BitString.propagate: the source/link recurrence, initialized with false.
• Cslib.BitString.keyLinks: link adjacent equal keys.

Main results

• Cslib.BitString.propagate_eq_true_iff: characterization by a connected true source.
• Cslib.BitString.propagate_sorted_eq_true_iff: on sorted keys, the output is the OR of the sources in the equal-key run ending at the last processed record.

References

• Adapted from MassProduction/Nonuniform/{Propagation,SortedPropagation}.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.BitString.propagate (source link : ℕ → Bool) : ℕ → Bool

The propagated value after processing a prefix, starting with false.

theorem Cslib.BitString.propagate_congr {source source' link link' : ℕ → Bool} (count : ℕ) (hs : ∀ (i : ℕ), i < count → source i = source' i) (hl : ∀ (i : ℕ), i < count → link i = link' i) : propagate source link count = propagate source' link' count

Propagation depends only on the source and link bits in its processed prefix.

theorem Cslib.BitString.propagate_eq_true_iff (source link : ℕ → Bool) (count : ℕ) : propagate source link count = true ↔ ∃ (start : ℕ), start < count ∧ source start = true ∧ ∀ (index : ℕ), start < index → index < count → link index = true

A true value has a true source connected to the end by uninterrupted true links.

def Cslib.BitString.keyLinks {κ : Type u_1} [DecidableEq κ] (key : ℕ → κ) (index : ℕ) : Bool

Adjacent records are linked precisely when their keys agree; the first link is false.

theorem Cslib.BitString.propagate_sorted_eq_true_iff {κ : Type u_1} [LinearOrder κ] [DecidableEq κ] (key : ℕ → κ) (source : ℕ → Bool) (count : ℕ) (sorted : MonotoneOn key (Set.Iio count)) : propagate source (keyLinks key) count = true ↔ ∃ (start : ℕ), start < count ∧ source start = true ∧ key start = key (count - 1)

In a sorted prefix, propagation reports exactly the true sources having the last key. The prefix may be empty. No uniqueness of sources or keys is required, and no order is required beyond the prefix. The explicit equality instance retains the caller's executable equality test when it differs from the one inherited from the order.