Reference · Finite sums

rainbow.math.sums.selected-minimum

Finite sumssrc/rainbow/math/sums/selected_minimum.clj0 definitions, 2 theorems

A one-hot selected minimum among non-excluded entries. The exclusion penalty can have either sign; the dominance premise is used only where exclusion is zero.

Depends onmath.sums.lp-boundsmath.rational.signed.one-hot-selects

signed/unit-bounds-polynomial-is-binary :
  (x : ℚ)
  (nonnegative : 0 ≤ x)
  (upper : x ≤ 1)
  (polynomial : x · (1 + signed/negate x) ≤ 0)
  → proposition/disjunction (x = 0) (x = 1)

signed/one-hot-excluded-minimum :
  (weights excluded values : ℕ → ℚ) (value penalty : ℚ) (n : ℕ)
  (nonnegative : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ weights idx)
  (binary : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), proposition/disjunction (weights idx = 0) (weights idx = 1))
  (unit-sum : signed/expr-sum-value weights n = 1)
  (weighted-value : value = signed/expr-sum-value (fun z => weights z · values z) n)
  (excluded-nonnegative : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ excluded idx)
  (disjoint : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), weights idx + excluded idx ≤ 1)
  (dominates : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), value ≤ values idx + penalty · excluded idx)
  → proposition/conjunction (existence) (∀ (entry : ℕ), ∀ (below : nat/strict-below entry n), ∀ (available : excluded entry = 0), value ≤ values entry)
  where existence := proposition/existence ℕ (fun entry => proposition/conjunction (nat/strict-below entry n) (proposition/conjunction (weights entry = 1) (proposition/conjunction (excluded entry = 0) (value = values entry))))