Reference · Finite sums

rainbow.math.sums.one-hot-index

Finite sumssrc/rainbow/math/sums/one_hot_index.clj0 definitions, 3 theorems

Every selected index reads every one-hot weighted sum; every distinct index is zero.

Depends onmath.sums.binary-conflictsmath.rational.signed.one-hot-selectsmath.rational.signed.one-hot-unique

signed/one-hot-selected-index-reads :
  (W F : ℕ → ℚ) (n : ℕ)
  (binary : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), proposition/disjunction (W idx = 0) (W idx = 1))
  (unit : signed/expr-sum-value W n = 1)
  (w : ℕ) (bound : nat/strict-below w n)
  (selected : W w = 1)
  → signed/expr-sum-value (fun z => W z · F z) n = F w

signed/one-hot-distinct-index-zero :
  (W : ℕ → ℚ) (n : ℕ)
  (binary : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), proposition/disjunction (W idx = 0) (W idx = 1))
  (unit : signed/expr-sum-value W n = 1)
  (w : ℕ) (hw : nat/strict-below w n)
  (selected : W w = 1)
  (j : ℕ) (hj : nat/strict-below j n) (distinct : proposition/negation (w = j))
  → W j = 0

signed/one-and-zero-indices-distinct :
  (W : ℕ → ℚ) (w j : ℕ)
  (one : W w = 1)
  (zero : W j = 0)
  → proposition/negation (w = j)