Skip to content
Flexiana
Menu
Solutions
How we work
Research
Work
Products
Company
Bring us a hard problem
Rainbow docs menu

Reference · Non-negative rationals

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

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_vector_step_covered.clj0 definitions, 1 theorems

Covered elimination step (the vacuity fix, consumer migration): one step in the held next-variable representation carrying the covering conjunct. farkas-vector-step produced a vacuous held-goal EXISTS (l,u), held -- the empty pair satisfies it. This variant composes farkas-vector-round-covered with the unit-column re-presentation, threading the covering through: the round gives affine lists with length(l)+length(u) = length(packed rows); repr preserves length (farkas-vector-unit-repr-length); so the re-presented next-variable lists satisfy length(repr l)+length(repr u) = length(packed rows). Hence the step's held-goal carries that covering and is NOT empty-satisfiable. Still DIRECTION-NEUTRAL: this fixes the step's existential vacuity; it does not touch the Feasible predicate whose uniformity in k is the Option 1/2 collapse (feasible-step / eliminate remain unmigrated). Built additively; the original farkas-vector-step is untouched. Depends on farkas-vector-round-covered, so it breaks loudly if that keystone chain stops holding. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-vector-round-coveredmath.rational.nnrat.farkas-vector-unit-columnmath.rational.nnrat.farkas-vector-unit-repr-length

nnrat/farkas-vector-step-covered

TheoremFor all inputsNo axiomsSource, line 114

nnrat/farkas-vector-step-covered :
  (lowers uppers : List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0))))))
  (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-cross-vectors-lowers-hold (nnrat/farkas-adapter-map-uppers (first pr) 1) x2) (nnrat/farkas-cross-vectors-uppers-hold (nnrat/farkas-adapter-map-uppers (second pr) 1) x2)) (algebra/nat-add (list/length (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0))))) (first pr)) (list/length (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0))))) (second pr)) = length))
  where Product := data/Product (List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0)))))) (List (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 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0)))))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (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 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0)))))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0))))))
  where uppers := nnrat/farkas-adapter-map-uppers lowers x2
  where uppers₅ := nnrat/farkas-adapter-map-uppers uppers x2

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