Reference · Non-negative rationals

rainbow.math.rational.nnrat.lp-strong-duality-general

Non-negative rationalssrc/rainbow/math/rational/nnrat/lp_strong_duality_general.clj0 definitions, 8 theorems

Constructive strong duality for a parametric scalar LP. For positive rationals a and b and an arbitrary nonnegative rational c, maximize c*x subject to a*x <= b minimize b*y subject to c <= a*y, the matching-dual system for a primal-feasible x normalizes to the finite Farkas chain interval c/a <= y <= (c*x)/b. The encoding is exact: a feasible zero-gap dual gives a chain witness, while a chain witness proves that the canonical y=(c*x)/b is dual feasible and has zero gap. The constructive chain alternative therefore gives either a zero-gap dual (and primal optimality) or both a refutation of every matching dual and the reduced-system Farkas infeasibility certificate. At x=b/a and y=c/a the interval is inhabited, yielding strong duality and primal/dual optimality for the whole positive-coefficient scalar family. All declarations are native proof data and axiom-free.

Depends onmath.rational.nnrat.farkas-alternativemath.rational.nnrat.order-scalemath.rational.nnrat.multiply-right-monotone

nnrat/lp-single-constraint-weak-duality :
  (a b c x y : ℚ≥0)
  (hp : a · x ≤ b)
  (hd : c ≤ a · y)
  → c · x ≤ b · y

nnrat/lp-single-constraint-optimality-certificate :
  (a b c x y : ℚ≥0)
  (hp : a · x ≤ b)
  (hd : c ≤ a · y)
  (hgap : c · x = b · y)
  (x-alt : ℚ≥0)
  (hp-alt : a · x-alt ≤ b)
  → c · x-alt ≤ c · x

nnrat/lp-single-constraint-dual-optimality-certificate :
  (a b c x y : ℚ≥0)
  (hp : a · x ≤ b)
  (hd : c ≤ a · y)
  (hgap : c · x = b · y)
  (y-alt : ℚ≥0)
  (hd-alt : c ≤ a · y-alt)
  → b · y ≤ b · y-alt

nnrat/lp-single-positive-constraint-dual-match-encodes :
  (ap adp bp bdp : ℕ) (c x : ℚ≥0)
  (matching : proposition/existence ℚ≥0 (fun y => proposition/conjunction (c ≤ nnrat/make (data/succ ap) adp · y) (c · x = nnrat/make (data/succ bp) bdp · y)))
  → nnrat/farkas-elim-chain-solvable [] [divide₁] (divide) []
  where divide := nnrat/divide (c · x) (nnrat/make (data/succ bp) bdp)
  where divide₁ := nnrat/divide c (nnrat/make (data/succ ap) adp)

nnrat/lp-single-positive-constraint-dual-match-extracts :
  (ap adp bp bdp : ℕ) (c x : ℚ≥0)
  (hp : nnrat/make (data/succ ap) adp · x ≤ nnrat/make (data/succ bp) bdp)
  (solution : nnrat/farkas-elim-chain-solvable [] [divide₁] (divide) [])
  → proposition/existence ℚ≥0 (fun y => proposition/conjunction (c ≤ nnrat/make (data/succ ap) adp · y) (proposition/conjunction (c · x = nnrat/make (data/succ bp) bdp · y) (∀ (x-alt : ℚ≥0), ∀ (hp-alt : nnrat/make (data/succ ap) adp · x-alt ≤ nnrat/make (data/succ bp) bdp), c · x-alt ≤ c · x)))
  where divide := nnrat/divide (c · x) (nnrat/make (data/succ bp) bdp)
  where divide₁ := nnrat/divide c (nnrat/make (data/succ ap) adp)

nnrat/lp-single-positive-constraint-dual-match-encoding-iff :
  (ap adp bp bdp : ℕ) (c x : ℚ≥0)
  → proposition/conjunction (existence → solvable) (solvable → existence)
  where existence := proposition/existence ℚ≥0 (fun y => proposition/conjunction (c ≤ nnrat/make (data/succ ap) adp · y) (c · x = nnrat/make (data/succ bp) bdp · y))
  where solvable := nnrat/farkas-elim-chain-solvable [] [nnrat/divide c (nnrat/make (data/succ ap) adp)] (nnrat/divide (c · x) (nnrat/make (data/succ bp) bdp)) []

nnrat/lp-single-positive-constraint-strong-duality-or-farkas-certificate :
  (ap adp bp bdp : ℕ) (c x : ℚ≥0)
  (hp : nnrat/make (data/succ ap) adp · x ≤ nnrat/make (data/succ bp) bdp)
  → proposition/disjunction (existence) (conjunction)
  where conjunction := proposition/conjunction (proposition/existence ℚ≥0 (fun y => proposition/conjunction (c ≤ nnrat/make (data/succ ap) adp · y) (c · x = nnrat/make (data/succ bp) bdp · y)) → proposition/falsity) (nnrat/farkas-elim-chain-solvable [] [nnrat/divide c (nnrat/make (data/succ ap) adp)] (nnrat/divide (c · x) (nnrat/make (data/succ bp) bdp)) [] → proposition/falsity)
  where existence := proposition/existence ℚ≥0 (fun y => proposition/conjunction (c ≤ nnrat/make (data/succ ap) adp · y) (proposition/conjunction (c · x = nnrat/make (data/succ bp) bdp · y) (∀ (x-alt : ℚ≥0), ∀ (hp-alt : nnrat/make (data/succ ap) adp · x-alt ≤ nnrat/make (data/succ bp) bdp), c · x-alt ≤ c · x)))

nnrat/lp-single-positive-constraint-strong-duality :
  (ap adp bp bdp : ℕ) (c : ℚ≥0)
  → proposition/conjunction (nnrat/make (data/succ ap) adp · nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp) ≤ nnrat/make (data/succ bp) bdp) (conjunction)
  where conjunction := proposition/conjunction (c ≤ nnrat/make (data/succ ap) adp · nnrat/divide c (nnrat/make (data/succ ap) adp)) (proposition/conjunction (c · nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp) = nnrat/make (data/succ bp) bdp · nnrat/divide c (nnrat/make (data/succ ap) adp)) (proposition/conjunction (∀ (x-alt : ℚ≥0), ∀ (hp-alt : nnrat/make (data/succ ap) adp · x-alt ≤ nnrat/make (data/succ bp) bdp), c · x-alt ≤ c · nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp)) (proposition/conjunction (∀ (y-alt : ℚ≥0), ∀ (hd-alt : c ≤ nnrat/make (data/succ ap) adp · y-alt), nnrat/make (data/succ bp) bdp · nnrat/divide c (nnrat/make (data/succ ap) adp) ≤ nnrat/make (data/succ bp) bdp · y-alt) (nnrat/farkas-elim-chain-solvable [] [nnrat/divide c (nnrat/make (data/succ ap) adp)] (nnrat/divide (c · nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp)) (nnrat/make (data/succ bp) bdp)) []))))