Reference · Signed rationals

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

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

THE ONE-HOT ATTAINMENT LEMMA WITH A KEEP OPTION, in the sign convention the relaxation checkers use (Bellman-Ford round, Dijkstra step, Floyd-Warshall round). Such a checker certifies a new value v' as the minimum of a 'keep' candidate and k arc candidates. v' is a lower bound of each, so every GAP v' - candidate is <= 0. A 0/1 witness y (keep) and Z_i (arc i) sums to 1, and the witnessed gaps sum to 0: signed/one-hot-keep-attained : 0 <= y, y ~ 0 \/ y ~ 1, a <= 0, (forall i < k, 0 <= Z i), (forall i < k, Z i ~ 0 \/ Z i ~ 1), (forall i < k, B i <= 0), y + expr-sum-value Z k ~ 1, y * a + expr-sum-value (fun i. Z i * B i) k ~ 0 -> (y ~ 1 /\ a ~ 0) \/ exists i < k, Z i ~ 1 /\ B i ~ 0 so the minimum is attained at the keep candidate or at a witnessed arc. The proof is the same strengthened induction as signed/one-hot-attained with the order reversed: a sum of nonpositive terms is <= 0, and two nonpositive terms adding to ~ 0 are both ~ 0. That last step is proved here from the order laws (0 ~ a + b <= a + 0 ~ a, then antisymmetry).

Depends onmath.rational.signed.one-hot-attained

signed/one-hot-attained-nonpositive-strengthened :
  (W B : ℕ → ℚ) (k : ℕ)
  (hw : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), 0 ≤ W i)
  (h01 : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), proposition/disjunction (W i = 0) (W i = 1))
  (hb : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), B i ≤ 0)
  → proposition/conjunction (value ≤ 0) (value = 0 → disjunction)
  where disjunction := proposition/disjunction (signed/expr-sum-value W k = 0) (proposition/existence ℕ (fun i => proposition/conjunction (nat/strict-below i k) (proposition/conjunction (W i = 1) (B i = 0))))
  where value := signed/expr-sum-value (fun i => W i · B i) k

signed/one-hot-keep-attained :
  (y a : ℚ) (Z B : ℕ → ℚ) (k : ℕ)
  (hy : 0 ≤ y)
  (hy01 : proposition/disjunction (y = 0) (y = 1))
  (ha : a ≤ 0)
  (hz : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), 0 ≤ Z i)
  (hz01 : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), proposition/disjunction (Z i = 0) (Z i = 1))
  (hb : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), B i ≤ 0)
  (hsum : y + signed/expr-sum-value Z k = 1)
  (hzero : y · a + signed/expr-sum-value (fun i => Z i · B i) k = 0)
  → proposition/disjunction (proposition/conjunction (y = 1) (a = 0)) (existence)
  where existence := proposition/existence ℕ (fun i => proposition/conjunction (nat/strict-below i k) (proposition/conjunction (Z i = 1) (B i = 0)))