Reference · Non-negative rationals

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

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_vector_adapter_list.clj2 definitions, 1 theorems

The unified representation, partition bridge adapter (per-upper list) : turn one round's per-lower reduced conditions into the flat descriptor fold the bridge consumes. farkas-cross-vectors-reduced (brick 3's one-lower fold) proves, for one lower row against a list of upper rows, that every pairwise reduced both-sides vector condition (reduced-at) holds -- a NESTED conjunction fold in the coefficient-vector (list-u) representation. The bridge fold (farkas-vector-partition-fold) instead wants a FLAT all-input-rows fold over descriptors (l1,u1,bL,bU,a2l,a2u,rl,ru). The two are the same proposition once each upper carries its next-variable coefficient explicitly: a next-variable constraint is (coeff,(bound,(a2,rest))), whose cross-vectors tail is cons((a2,x2),rest); for such an upper, reduced-at(map-to-c upper) is DEFINITIONALLY input-row(descriptor(lower, upper)) at x2 (same coefficients, same scaled tails). nnrat/farkas-vector-adapter-list is the List.rec transporting the nested fold to the flat one, conjunct by conjunct via that defeq: given farkas-cross-vectors-reduced holds for the mapped upper list, all-input-rows holds for the per-upper descriptor list (nnrat/farkas-adapter-descs-of-lower = map (upper -> descriptor(lower,upper))). Folding this over the lower list next gives the whole round's descriptor list, which the bridge fold + the already-proved partition turn into the next round's affine system. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-vector-partition-foldmath.rational.nnrat.farkas-cross-vectors-list

nnrat/farkas-adapter-map-uppers :
  (x₁ : List (data/Product ℚ≥0 (Product))) (x₂ : ℚ≥0)
  → List (data/Product ℚ≥0 (Product₁))
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0)))
  where Product₁ := data/Product (List (data/Product ℚ≥0 ℚ≥0)) ℚ≥0

nnrat/farkas-adapter-descs-of-lower :
  (x₁ x₂ x₃ : ℚ≥0) (x₄ : List (data/Product ℚ≥0 ℚ≥0))
  (x₅ : List (data/Product ℚ≥0 (Product₁)))
  → List (data/Product ℚ≥0 (Product))
  where Product := 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)))))))
  where Product₁ := data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0)))

nnrat/farkas-vector-adapter-list :
  (l-coeff b-l a2l : ℚ≥0) (rl : List (data/Product ℚ≥0 ℚ≥0))
  (uppers : List (data/Product ℚ≥0 (Product))) (x1 x2 : ℚ≥0)
  (h : nnrat/farkas-cross-vectors-reduced (uppers) x1 l-coeff (cons) b-l)
  → nnrat/farkas-vector-partition-input-rows (lower) x2
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0)))
  where cons := data/cons (data/Product ℚ≥0 ℚ≥0) (data/pair ℚ≥0 ℚ≥0 a2l x2) rl
  where lower := nnrat/farkas-adapter-descs-of-lower l-coeff b-l a2l rl uppers
  where uppers := nnrat/farkas-adapter-map-uppers uppers x2