Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.odd-cycle-cut

Lemmas behind operations-research checks src/rainbow/math/lemmas/odd_cycle_cut.clj0 definitions, 8 theorems

General lemmas: odd cycle cut. The mathematical facts the corresponding checks rest on, each checked by the kernel.

signed/of-nat-add

TheoremFor all inputsNo axiomsSource

signed/of-nat-add :
  (oa-a oa-b : ℕ)
  → signed/from-nnrat (nnrat/make (algebra/nat-add oa-a oa-b) 0) = signed/from-nnrat (nnrat/make oa-a 0) + signed/from-nnrat (nnrat/make oa-b 0)

+ = signed/add= = signed/equivalent: equality of rational valuesℕ = data/Nat

signed/of-nat-monotone

TheoremFor all inputsNo axiomsSource

signed/of-nat-monotone :
  (om-a om-b : ℕ)
  (om-h : om-a ≤ om-b)
  → signed/from-nnrat (nnrat/make om-a 0) ≤ signed/from-nnrat (nnrat/make om-b 0)

ℕ = data/Nat≤ = signed/at-most

signed/of-nat-double

TheoremFor all inputsNo axiomsSource

signed/of-nat-double :
  (od-k : ℕ)
  → signed/from-nnrat (nnrat/make (nat/multiply 2 od-k) 0) = signed/from-nnrat (nnrat/make od-k 0) + signed/from-nnrat (nnrat/make od-k 0)

+ = signed/add= = signed/equivalent: equality of rational valuesℕ = data/Nat

signed/of-nat-half-floor

TheoremFor all inputsNo axiomsSource

signed/of-nat-half-floor :
  (hf-n hf-k : ℕ)
  (hf-h : signed/from-nnrat (nnrat/make hf-n 0) + signed/from-nnrat (nnrat/make hf-n 0) ≤ signed/from-nnrat (nnrat/make hf-k 0) + signed/from-nnrat (nnrat/make hf-k 0) + 1)
  → signed/from-nnrat (nnrat/make hf-n 0) ≤ signed/from-nnrat (nnrat/make hf-k 0)

+ = signed/add1 = signed/oneℕ = data/Nat≤ = signed/at-most

signed/zero-one-sum-of-nat

TheoremFor all inputsNo axiomsSource

signed/zero-one-sum-of-nat :
  (zs-f : ℕ → ℚ) (zs-n : ℕ)
  (zs-h : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx zs-n), proposition/disjunction (zs-f idx = 0) (zs-f idx = 1))
  → proposition/existence ℕ (fun cnt => signed/expr-sum-value zs-f zs-n = signed/from-nnrat (nnrat/make cnt 0))

0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational valuesℕ = data/Natℚ = signed/SignedRational

signed/odd-cycle-count

TheoremFor all inputsNo axiomsSource

signed/odd-cycle-count :
  (oc-z : ℕ → ℚ) (oc-k : ℕ)
  (oc-01 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ (nat/multiply 2 oc-k))), proposition/disjunction (oc-z idx = 0) (oc-z idx = 1))
  (oc-adj : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ (nat/multiply 2 oc-k))), oc-z idx + oc-z (data/succ idx) ≤ 1)
  (oc-close : oc-z (data/succ (nat/multiply 2 oc-k)) = oc-z 0)
  → signed/expr-sum-value oc-z (data/succ (nat/multiply 2 oc-k)) ≤ signed/from-nnrat (nnrat/make oc-k 0)

+ = signed/add0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational valuesℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most

signed/odd-cycle-step

TheoremFor all inputsNo axiomsSource

signed/odd-cycle-step :
  (st-n : ℕ) (st-a st-b : ℕ → ℚ) (st-e : ℕ → ℕ → ℚ) (st-y : ℕ → ℚ)
  (st-a01 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx st-n), st-a idx · (1 + signed/negate (st-a idx)) = 0)
  (st-asum : signed/expr-sum-value st-a st-n = 1)
  (st-b01 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx st-n), st-b idx · (1 + signed/negate (st-b idx)) = 0)
  (st-bsum : signed/expr-sum-value st-b st-n = 1)
  (st-step : signed/expr-sum-value (fun st-u => st-a st-u · signed/expr-sum-value (fun st-v => st-b st-v · st-e st-u st-v) st-n) st-n = 1)
  (st-y01 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx st-n), st-y idx · (1 + signed/negate (st-y idx)) = 0)
  (st-free : ∀ (fu : ℕ), ∀ (fu-lt : nat/strict-below fu st-n), ∀ (fv : ℕ), ∀ (fv-lt : nat/strict-below fv st-n), st-y fu · st-y fv · st-e fu fv = 0)
  → proposition/conjunction (disjunction) (signed/expr-sum-value (fun wi => st-a wi · st-y wi) st-n + value ≤ 1)
  where disjunction := proposition/disjunction (signed/expr-sum-value (fun wi => st-a wi · st-y wi) st-n = 0) (signed/expr-sum-value (fun wi => st-a wi · st-y wi) st-n = 1)
  where value := signed/expr-sum-value (fun wi => st-b wi · st-y wi) st-n

+ = signed/add0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most

signed/odd-cycle-separates

TheoremFor all inputsNo axiomsSource

signed/odd-cycle-separates :
  (sp-t : ℚ) (sp-k : ℕ)
  (sp-v : 1 ≤ data/Bool.rec (fun x₄ => ℚ) 1 0 (most))
  (sp-le : sp-t ≤ signed/from-nnrat (nnrat/make sp-k 0))
  → proposition/falsity
  where most := signed/decide-at-most (signed/from-nnrat 2 · sp-t) (signed/from-nnrat (nnrat/make (nat/multiply 2 sp-k) 0))

0 = signed/zero1 = signed/one· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most