Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-vector-round-covered

Non-negative rationals src/rainbow/math/rational/nnrat/farkas_vector_round_covered.clj0 definitions, 1 theorems

Covered coefficient-vector round (the vacuity fix, consumer migration): one Fourier-Motzkin round on the covering-strengthened partition keystone. farkas-vector-round produced the vacuous goal EXISTS (l,u), sat -- inherited from farkas-partition-list-necessary. This variant applies nnrat/farkas-partition-list-covered instead, so its conclusion carries the covering conjunct length(l)+length(u) = length(packed-list (descs-bilist lowers uppers)) and is not empty-satisfiable. Same composition as farkas-vector-round (cross-vectors-all-reduced -> adapter-bilist -> partition-fold), only the final partition is the covered one. This is the round's EXISTENTIAL-vacuity fix and is DIRECTION-NEUTRAL: it is independent of the uniform-Feasible collapse (Option 1/2), which lives one layer up in step/feasible-step/eliminate and is untouched here. Built additively; the original farkas-vector-round and the step/eliminate wiring are not disturbed. This proof DEPENDS on the covered keystone (its value applies partition-list-covered), so it breaks loudly if the keystone stops holding. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-vector-adapter-bilist math.rational.nnrat.farkas-partition-covered

nnrat/farkas-vector-round-covered

TheoremFor all inputsNo axiomsSource, line 102

nnrat/farkas-vector-round-covered :
  (lowers uppers : List (Product₄)) (x1 x2 : ℚ≥0)
  (lh : nnrat/farkas-cross-vectors-lowers-hold (uppers) x1)
  (uh : nnrat/farkas-cross-vectors-uppers-hold (uppers₆) x1)
  → proposition/existence (Product) (fun pr => proposition/conjunction (proposition/conjunction (nnrat/farkas-lowers-satisfied (first pr) x2) (nnrat/farkas-elim-affine-rows-satisfied (second pr) x2)) (algebra/nat-add (list/length (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)) (first pr)) (list/length (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)) (second pr)) = length))
  where Product := data/Product (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  where Product₄ := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0))))
  where first := product/first (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  where length := list/length (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (nnrat/farkas-vector-partition-packed (nnrat/farkas-adapter-descs-bilist lowers uppers))
  where second := product/second (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  where uppers := nnrat/farkas-adapter-map-uppers lowers x2
  where uppers₆ := nnrat/farkas-adapter-map-uppers uppers x2

= = equality/EqList = data/Listℚ≥0 = nnrat/NonnegativeRational