Reference · Signed rationals

rainbow.math.rational.signed.one-hot-unique

Signed rationalssrc/rainbow/math/rational/signed/one_hot_unique.clj0 definitions, 3 theorems

A ONE-HOT SELECTOR SELECTS ONE INDEX. Nonnegative weights summing to ~1 cannot have two distinct entries ~1: signed/term-below-sum : (forall i < k, 0 <= S i) -> p < k -> S p <= sum S k signed/two-terms-below-sum: (forall i < k, 0 <= S i) -> p < q -> q < k -> S p + S q <= sum S k signed/one-hot-unique : (forall i < k, 0 <= S i) -> sum S k ~ 1 -> p < k -> q < k -> S p ~ 1 -> S q ~ 1 -> p = q since distinct p and q would give 1 + 1 <= sum ~ 1. Consumer: the Floyd-Warshall chain bridge. A chain names its pivots P t, and uniqueness identifies the reading's existential pivot with them.

Depends onmath.rational.signed.one-hot-selectsmath.nat.pigeonholemath.sums.value-algebra

signed/term-below-sum :
  (S : ℕ → ℚ) (k : ℕ)
  (hn : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), 0 ≤ S i)
  (p : ℕ) (hp : nat/strict-below p k)
  → S p ≤ signed/expr-sum-value S k

signed/two-terms-below-sum :
  (S : ℕ → ℚ) (k : ℕ)
  (hn : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), 0 ≤ S i)
  (p q : ℕ) (hpq : nat/strict-below p q) (hq : nat/strict-below q k)
  → S p + S q ≤ signed/expr-sum-value S k

signed/one-hot-unique :
  (S : ℕ → ℚ) (k : ℕ)
  (hn : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), 0 ≤ S i)
  (hsum : signed/expr-sum-value S k = 1)
  (p q : ℕ) (hp : nat/strict-below p k) (hq : nat/strict-below q k)
  (sp : S p = 1)
  (sq : S q = 1)
  → p = q