Propagation along sorted equal-key runs

In a sorted array, equal keys occupy an interval. Linking adjacent equal keys therefore propagates a source bit to exactly the later records having that key, regardless of how many such records there are.

def Algebraic.MassProduction.Nonuniform.Propagation.keyLinks {Key : Type u_1} [DecidableEq Key] (key : ℕ → Key) (index : ℕ) : Bool

Adjacent records are linked exactly when their keys are equal.

Equations

• Algebraic.MassProduction.Nonuniform.Propagation.keyLinks key index = if index = 0 then false else decide (key (index - 1) = key index)

theorem Algebraic.MassProduction.Nonuniform.Propagation.value_sorted_eq_true_iff {Key : Type u_1} [LinearOrder Key] (key : ℕ → Key) (source : ℕ → Bool) (count : ℕ) (countPositive : 0 < count) (sorted : ∀ {left right : ℕ}, left ≤ right → right < count → key left ≤ key right) : value source (keyLinks key) count = true ↔ ∃ start < count, source start = true ∧ key start = key (count - 1)

The segmented recurrence on sorted keys reports precisely the source bits in the equal-key run ending at the last processed record.