Reference · Non-negative rationals

rainbow.math.rational.nnrat.lp-complementary

Non-negative rationalssrc/rainbow/math/rational/nnrat/lp_complementary.clj0 definitions, 2 theorems

Complementary slackness for LP over nonnegative rationals -- the KKT optimality characterization, now a named machine-checked theorem. With subtraction-free feasibility (primal (A x)_i + s_i ~ b_i, dual c_j + r_j ~ (Aᵀy)_j) and a ZERO duality gap (b.y ~ c.x): nnrat/lp-complementary-slackness-dual : sum_j r_j x_j ~ 0 nnrat/lp-complementary-slackness-primal : sum_i s_i y_i ~ 0 i.e. at a zero-gap (hence optimal) primal/dual pair the total reduced-cost*value and slack*multiplier sums vanish; since each product is nonnegative, map-sum-zero-at-split then forces every individual r_e x_e and s_e y_e to 0 (a variable is 0 or its constraint is tight). Proof: the gap-decomposition gives b.y ~ c.x + (SR + SS); zero gap + add-cancel-to-zero forces (SR + SS) ~ 0; add-zero-split splits it to SR ~ 0 and SS ~ 0. (Per-term extraction to any individual r_e x_e ~ 0 is nnrat/map-sum-zero-at-split, in nnrat-map-sum-zero.) Native and axiom-free; chains nnrat-lp-gap and nnrat-add-cancel-zero on d63.

Depends onmath.rational.nnrat.lp-gapmath.rational.nnrat.add-cancel-zero

nnrat/lp-complementary-slackness-dual.{u} :
  (RowT ColT : Type u) (A : RowT → ColT → ℚ≥0) (b : RowT → ℚ≥0) (c x : ColT → ℚ≥0)
  (y s : RowT → ℚ≥0) (r : ColT → ℚ≥0) (rows : List RowT) (cols : List ColT)
  (hp : ∀ (i : RowT), nnrat/map-sum ColT (fun j => A i j · x j) cols + s i = b i)
  (hd : ∀ (j : ColT), c j + r j = nnrat/map-sum RowT (fun i => A i j · y i) rows)
  (hgap : nnrat/map-sum RowT (fun i => b i · y i) rows = nnrat/map-sum ColT (fun j => c j · x j) cols)
  → nnrat/map-sum ColT (fun j => r j · x j) cols = 0

nnrat/lp-complementary-slackness-primal.{u} :
  (RowT ColT : Type u) (A : RowT → ColT → ℚ≥0) (b : RowT → ℚ≥0) (c x : ColT → ℚ≥0)
  (y s : RowT → ℚ≥0) (r : ColT → ℚ≥0) (rows : List RowT) (cols : List ColT)
  (hp : ∀ (i : RowT), nnrat/map-sum ColT (fun j => A i j · x j) cols + s i = b i)
  (hd : ∀ (j : ColT), c j + r j = nnrat/map-sum RowT (fun i => A i j · y i) rows)
  (hgap : nnrat/map-sum RowT (fun i => b i · y i) rows = nnrat/map-sum ColT (fun j => c j · x j) cols)
  → nnrat/map-sum RowT (fun i => s i · y i) rows = 0