Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.matching-cover-duality

Lemmas behind operations-research checkssrc/rainbow/math/lemmas/matching_cover_duality.clj0 definitions, 3 theorems

General lemmas: matching cover duality. The mathematical facts the corresponding checks rest on, each checked by the kernel.

signed/square-of-boolean-polynomial :
  (x : ℚ)
  (bit : x · (1 + signed/negate x) = 0)
  → x = x · x

signed/expr-sum-matching-cover-double-count :
  (X : ℕ → ℕ → ℚ) (L R : ℕ → ℚ) (p q : ℕ)
  → signed/expr-sum-value (fun row => signed/expr-sum-value (fun column-index => (fun i => fun j => X i j · (L i + R j)) row column-index) q) p = signed/expr-sum-value (fun i => L i · (fun row => signed/expr-sum-value (fun column-index => X row column-index) q) i) p + signed/expr-sum-value (fun i => R i · (fun col => signed/expr-sum-value (fun row-index => X row-index col) p) i) q

signed/expr-sum-matching-cover-weak-duality :
  (X : ℕ → ℕ → ℚ) (L R : ℕ → ℚ) (p q : ℕ)
  (nonnegative : ∀ (u : ℕ), ∀ (hu : nat/strict-below u p), ∀ (v : ℕ), ∀ (hv : nat/strict-below v q), 0 ≤ X u v)
  (bits : ∀ (u : ℕ), ∀ (hu : nat/strict-below u p), ∀ (v : ℕ), ∀ (hv : nat/strict-below v q), X u v · (1 + signed/negate (X u v)) = 0)
  (covered : ∀ (u : ℕ), ∀ (hu : nat/strict-below u p), ∀ (v : ℕ), ∀ (hv : nat/strict-below v q), X u v ≤ L u + R v)
  (rows : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx p), (fun row => signed/expr-sum-value (fun column-index => X row column-index) q) idx ≤ 1)
  (cols : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx q), (fun col => signed/expr-sum-value (fun row-index => X row-index col) p) idx ≤ 1)
  (left : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx p), 0 ≤ L idx)
  (right : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx q), 0 ≤ R idx)
  → signed/expr-sum-value (fun row => signed/expr-sum-value (fun column-index => X row column-index) q) p ≤ signed/expr-sum-value L p + signed/expr-sum-value R q