Reference · Signed rationals

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

Signed rationalssrc/rainbow/math/rational/signed/one_hot_selects.clj0 definitions, 2 theorems

THE ONE-HOT VALUE SELECTOR, the shared Level-3 reading of every checker that pins a value to a one-hot sum: Floyd-Warshall's pivot column and row, Dijkstra's chosen label and row, and the rest. 0/1 weights summing to 1 select one index, and every weighted sum then reads that index: signed/one-hot-selects : forall S k, (forall i < k, 0 <= S i) -> (forall i < k, S i ~ 0 \/ S i ~ 1) -> expr-sum-value S k ~ 1 -> exists p, p < k /\ S p ~ 1 /\ forall X, expr-sum-value (fun i. S i * X i) k ~ X p One p serves EVERY X, so a checker's column sum and row sum over the same selector read the same pivot. The proof is a three-way strengthened induction. After k terms, either the weights sum to ~ 0 and every weighted sum is ~ 0; or they sum to ~ 1 and a selected p reads every X; or they sum to at least 1 + 1. A step with S k ~ 0 keeps the case; S k ~ 1 moves case 0 to case 1 at p = k, and cases 1 and 2 to case 2. At the end a sum of ~ 1 rules out ~ 0 (1 is not 0) and >= 1 + 1 (1 + 1 <= 1 would give 1 <= 0).

Depends onmath.rational.signed.one-hot-keepmath.rational.signed.order-cancellation

signed/one-hot-selects-strengthened :
  (S : ℕ → ℚ) (k : ℕ)
  (hs : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), 0 ≤ S i)
  (h01 : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), proposition/disjunction (S i = 0) (S i = 1))
  → proposition/disjunction (conjunction) (disjunction)
  where conjunction := proposition/conjunction (signed/expr-sum-value S k = 0) (∀ (X : ℕ → ℚ), signed/expr-sum-value (fun i => S i · X i) k = 0)
  where disjunction := proposition/disjunction (proposition/conjunction (signed/expr-sum-value S k = 1) (proposition/existence ℕ (fun p => proposition/conjunction (nat/strict-below p k) (proposition/conjunction (S p = 1) (∀ (X : ℕ → ℚ), signed/expr-sum-value (fun i => S i · X i) k = X p))))) (1 + 1 ≤ signed/expr-sum-value S k)

signed/one-hot-selects :
  (S : ℕ → ℚ) (k : ℕ)
  (hs : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), 0 ≤ S i)
  (h01 : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), proposition/disjunction (S i = 0) (S i = 1))
  (hsum : signed/expr-sum-value S k = 1)
  → proposition/existence ℕ (fun p => proposition/conjunction (nat/strict-below p k) (proposition/conjunction (S p = 1) (∀ (X : ℕ → ℚ), signed/expr-sum-value (fun i => S i · X i) k = X p)))