Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.ncyc-infeasible

Lemmas behind operations-research checkssrc/rainbow/math/lemmas/ncyc_infeasible.clj0 definitions, 7 theorems

General lemmas: ncyc infeasible. The mathematical facts the corresponding checks rest on, each checked by the kernel.

Depends onmath.lemmas.indep-set-dualmath.sums.value-appendmath.nat.infinitemath.rational.nnrat.identitiesmath.nat.at-most-cancellationmath.rational.nnrat.order-equivalencemath.rational.nnrat.archimedeanmath.rational.nnrat.add-monotonemath.rational.nnrat.add-cancellationmath.rational.nnrat.additive-reassociationmath.rational.signed.order-transitivitymath.rational.signed.convergencemath.rational.signed.order-respectsmath.rational.signed.limit-uniquenessmath.rational.signed.strict-ordermath.rational.signed.multiplymath.rational.nnrat.multiply-commutemath.rational.nnrat.product-reassociationmath.rational.nnrat.distribute-rightmath.rational.nnrat.ringmath.rational.nnrat.multiply-monotonemath.rational.nnrat.order-differencemath.rational.signed.multiply-ordermath.rational.signed.equivalence-lawsmath.rational.nnrat.minmaxmath.rational.nnrat.farkas-elim-listmath.rational.signed.no-zero-divisorsmath.rational.signed.decide-ordermath.rational.signed.decide-reflexivemath.logic.boolean-andmath.rational.signed.decide-equivalencemath.rational.signed.decide-completenessmath.rational.signed.unit-lawsmath.nat.strict-below-splitmath.nat.strict-below-moremath.checksmath.nat.at-most-addmath.rational.nnrat.harmonic-convergencemath.nat.divmodmath.rational.signed.minmaxmath.rational.signed.minmax-algebramath.rational.signed.clampmath.rational.signed.deviation-rowsmath.rational.signed.absolutemath.rational.signed.absolute-algebramath.rational.signed.distancemath.nat.linear-ordermath.rational.signed.add-associativemath.nat.semiringmath.nat.multiply-zero-splitmath.rational.nnrat.multiply-zero-splitmath.nat.monusmath.rational.nnrat.monusmath.rational.nnrat.add-zero-splitmath.rational.nnrat.add-cancel-zeromath.finite.rational-argmaxmath.rational.nnrat.order-totalmath.rational.nnrat.multiply-difference-zeromath.linear.vector.norm-nonnegativemath.linear.vector.norm-zero-reflectionalgorithms.proofs.counterfactual-distance-separationalgorithms.proofs.counterfactual-distance-lawsmath.finite.matrixmath.linear.matrix.equivalencemath.linear.matrix.transposemath.linear.matrix.transpose-equivalencemath.linear.matrix.multiplymath.linear.matrix.multiply-shapemath.linear.matrix.composablemath.linear.matrix.composable-multiplymath.linear.vector.additive-unitsmath.linear.vector.shape-cancellationmath.linear.vector.shape-mapmath.linear.vector.shape-addmath.linear.vector.dot-additivemath.linear.vector.dot-bilinearmath.linear.vector.dot-negatemath.linear.vector.dot-subtractmath.linear.vector.dot-scalemath.linear.matrix.action-scalemath.rational.signed.multiply-nonzeromath.rational.signed.order-monotonemath.rational.signed.list-summath.rational.signed.multiply-monotonemath.rational.signed.map-sum-algebramath.rational.signed.negate-additivemath.rational.signed.lp-objective-negatemath.nat.pair-index-inversemath.sums.flow-cutmath.sums.nonneg-zeromath.rational.signed.multiply-associativemath.rational.signed.multiply-ringmath.rational.signed.distributive

signed/ncyc-term-split :
  (b w pu pv : ℚ)
  → b · (w + (pu + signed/negate pv)) = b · w + (pu · b + signed/negate (b · pv))

signed/ncyc-outer-split :
  (a w pu qb : ℚ)
  → a · (w + (pu + signed/negate qb)) = a · w + (a · pu + signed/negate (a · qb))

signed/ncyc-rearrange :
  (w qa qb : ℚ)
  (h : 0 ≤ w + (qa + signed/negate qb))
  → qb + signed/negate qa ≤ w

signed/ncyc-edge-slack :
  (pu pv w : ℚ)
  (h : pv ≤ pu + w)
  → 0 ≤ w + (pu + signed/negate pv)

signed/expr-sum-value-telescope :
  (q : ℕ → ℚ) (L : ℕ)
  → signed/expr-sum-value (fun tq => q (data/succ tq) + signed/negate (q tq)) L = q L + signed/negate (q 0)

signed/one-hot-step-potential-bound :
  (a b : ℕ → ℚ) (W E : ℕ → ℕ → ℚ) (p : ℕ → ℚ) (n : ℕ)
  (ha0 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ a idx)
  (hb0 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ b idx)
  (ha1 : signed/expr-sum-value (fun sa => a sa) n = 1)
  (hb1 : signed/expr-sum-value (fun sb => b sb) n = 1)
  (hE : ∀ (eu : ℕ), ∀ (eu-lt : nat/strict-below eu n), ∀ (ev : ℕ), ∀ (ev-lt : nat/strict-below ev n), E eu ev · (1 + signed/negate (E eu ev)) = 0)
  (hstep : signed/expr-sum-value (fun su => a su · signed/expr-sum-value (fun sv => b sv · E su sv) n) n = 1)
  (hpot : ∀ (pu : ℕ), ∀ (pu-lt : nat/strict-below pu n), ∀ (pv : ℕ), ∀ (pv-lt : nat/strict-below pv n), ∀ (pe : E pu pv = 1), p pv ≤ p pu + W pu pv)
  → signed/expr-sum-value (fun qu => b qu · p qu) n + signed/negate (signed/expr-sum-value (fun qu => a qu · p qu) n) ≤ signed/expr-sum-value (fun su => a su · signed/expr-sum-value (fun sv => b sv · W su sv) n) n

signed/closed-walk-potential-nonnegative :
  (P W E : ℕ → ℕ → ℚ) (p : ℕ → ℚ) (n L : ℕ)
  (hP0 : ∀ (ht : ℕ), ∀ (ht-lt : nat/strict-below ht (data/succ L)), ∀ (hu : ℕ), ∀ (hu-lt : nat/strict-below hu n), 0 ≤ P ht hu)
  (hrow : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ L)), signed/expr-sum-value (fun rw => P idx rw) n = 1)
  (hclose : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), P L idx = P 0 idx)
  (hE : ∀ (eu : ℕ), ∀ (eu-lt : nat/strict-below eu n), ∀ (ev : ℕ), ∀ (ev-lt : nat/strict-below ev n), E eu ev · (1 + signed/negate (E eu ev)) = 0)
  (hstep : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx L), signed/expr-sum-value (fun su => (fun rw => P idx rw) su · signed/expr-sum-value (fun sv => (fun rw => P (data/succ idx) rw) sv · E su sv) n) n = 1)
  (hpot : ∀ (pu : ℕ), ∀ (pu-lt : nat/strict-below pu n), ∀ (pv : ℕ), ∀ (pv-lt : nat/strict-below pv n), ∀ (pe : E pu pv = 1), p pv ≤ p pu + W pu pv)
  → 0 ≤ signed/expr-sum-value (fun wt => signed/expr-sum-value (fun su => (fun rw => P wt rw) su · signed/expr-sum-value (fun sv => (fun rw => P (data/succ wt) rw) sv · W su sv) n) n) L