Reference · Finite sums

rainbow.math.sums.bpath-cut

Finite sumssrc/rainbow/math/sums/bpath_cut.clj0 definitions, 4 theorems

Cut/exit proof support for bottleneck paths. All weights are signed; no nonnegative bottleneck premise. New lemmas over unchanged sums and selector definitions.

Depends onmath.sums.one-hot-factor

signed/one-hot-selects-binary-value :
  (bc-B bc-S : ℕ → ℚ) (bc-n : ℕ)
  (bc-bits : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bc-n), bc-B idx · (1 + signed/negate (bc-B idx)) = 0)
  (bc-unit : signed/expr-sum-value bc-B bc-n = 1)
  (bc-values-bits : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bc-n), bc-S idx · (1 + signed/negate (bc-S idx)) = 0)
  → value · (1 + signed/negate (value)) = 0
  where value := signed/expr-sum-value (fun oh-v => bc-B oh-v · bc-S oh-v) bc-n

signed/binary-sequence-exit :
  (bc-Z : ℕ → ℚ) (bc-M : ℕ)
  (bc-seq-bits : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ bc-M)), bc-Z idx · (1 + signed/negate (bc-Z idx)) = 0)
  (bc-start : bc-Z 0 = 1)
  (bc-end : bc-Z bc-M = 0)
  → proposition/existence ℕ (fun bc-exit => proposition/conjunction (nat/strict-below bc-exit bc-M) (proposition/conjunction (bc-Z bc-exit = 1) (bc-Z (data/succ bc-exit) = 0)))

signed/subtract-nonpositive-implies-at-most :
  (bc-x bc-y : ℚ)
  (bc-order : bc-x + signed/negate bc-y ≤ 0)
  → bc-x ≤ bc-y

signed/one-hot-cut-exit-weight-bound :
  (bc-A bc-B : ℕ → ℚ) (bc-E : ℕ → ℕ → ℚ) (bc-S : ℕ → ℚ) (bc-W : ℕ → ℕ → ℚ) (bc-n : ℕ)
  (bc-threshold : ℚ)
  (bc-abits : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bc-n), bc-A idx · (1 + signed/negate (bc-A idx)) = 0)
  (bc-aunit : signed/expr-sum-value bc-A bc-n = 1)
  (bc-bbits : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bc-n), bc-B idx · (1 + signed/negate (bc-B idx)) = 0)
  (bc-bunit : signed/expr-sum-value bc-B bc-n = 1)
  (bc-edge : signed/expr-sum-value (fun oh-u => bc-A oh-u · signed/expr-sum-value (fun oh-v => bc-B oh-v · (fun oh-v₁ => bc-E oh-u oh-v₁) oh-v) bc-n) bc-n = 1)
  (bc-inside : signed/expr-sum-value (fun oh-v => bc-A oh-v · bc-S oh-v) bc-n = 1)
  (bc-outside : signed/expr-sum-value (fun oh-v => bc-B oh-v · bc-S oh-v) bc-n = 0)
  (bc-crossing : ∀ (bc-u : ℕ), ∀ (bc-hu : nat/strict-below bc-u bc-n), ∀ (bc-v : ℕ), ∀ (bc-hv : nat/strict-below bc-v bc-n), bc-E bc-u bc-v · bc-S bc-u · ((1 + signed/negate (bc-S bc-v)) · (bc-threshold + signed/negate (bc-W bc-u bc-v))) ≤ 0)
  → bc-threshold ≤ signed/expr-sum-value (fun oh-u => bc-A oh-u · signed/expr-sum-value (fun oh-v => bc-B oh-v · (fun oh-v₁ => bc-W oh-u oh-v₁) oh-v) bc-n) bc-n