Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-vector-adapter-bilist

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

The unified representation, partition bridge adapter (the bilist) : turn one whole elimination round's reduced conditions into the flat descriptor fold the bridge consumes. farkas-cross-vectors-all-reduced-conds is the round's reduced conditions: a conjunction fold over the LOWER list, each entry the per-lower farkas-cross-vectors-reduced fold over the upper list. The per-upper adapter (nnrat/farkas-vector-adapter-list) already turns one lower's entry into the flat all-input-rows fold over that lower's descriptor list. This folds that over the lower list. Representing lowers and uppers as next-variable constraints (coeff,(bound,(a2,rest))) and mapping them to the round's list form at x2 (farkas-adapter-map-uppers), the round's all-reduced conditions imply all-input-rows of the concatenated per-lower descriptor lists (nnrat/farkas-adapter-descs-bilist = append the per-lower descriptor lists). Proof: List.rec over the lowers; each cons applies the per-upper adapter to its head entry and the induction hypothesis to the tail, then joins them with the append lemma nnrat/farkas-vector-input-rows-append (all-input-rows distributes over list/append). The concatenated descriptor list and this proof are exactly the bridge fold's input (farkas-vector-partition-fold), whose output is farkas-partition-list-necessary's input -- so composing adapter + fold + partition gives one closed coefficient-vector round: a feasible system in k+1 variables yields a feasible system in k. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-vector-adapter-listmath.rational.nnrat.farkas-cross-vectors-bilist

nnrat/farkas-vector-input-rows-append :
  (xs ys : List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product (List (data/Product ℚ≥0 ℚ≥0)) (List (data/Product ℚ≥0 ℚ≥0))))))))))
  (x2 : ℚ≥0) (hx : nnrat/farkas-vector-partition-input-rows xs x2)
  (hy : nnrat/farkas-vector-partition-input-rows ys x2)
  → nnrat/farkas-vector-partition-input-rows (append) x2
  where append := list/append (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product (List (data/Product ℚ≥0 ℚ≥0)) (List (data/Product ℚ≥0 ℚ≥0))))))))) xs ys

nnrat/farkas-vector-adapter-bilist :
  (lowers uppers : List (Product)) (x1 x2 : ℚ≥0)
  (h : nnrat/farkas-cross-vectors-all-reduced-conds (uppers) (uppers₃) x1)
  → nnrat/farkas-vector-partition-input-rows (bilist) x2
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0))))
  where bilist := nnrat/farkas-adapter-descs-bilist lowers uppers
  where uppers := nnrat/farkas-adapter-map-uppers lowers x2
  where uppers₃ := nnrat/farkas-adapter-map-uppers uppers x2