Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-partition-list

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

Piece (ii) brick 1: the dependent partition of a reduced disjunction system into a lower-list and an upper-list. One elimination round's output reduced-conditions is a fold of disjunctions. This threads it into the next round: given reduced-conditions holds at w, there EXIST a lower-row list and an upper-row list -- carried as one Product witness -- such that brick 5b's lower fold and brick 4's upper fold both hold at w. The lists' sizes are runtime-dependent (each row's lower/upper case is decided per row), so the partition is dependent. Proof: List.rec over the reduced rows; the base is two empty lists; each cons resolves the head via nnrat/farkas-partition-row (lower or upper affine constraint), constructs the corresponding brick 5b/4 row (a data/pair whose projections reduce to the constraint's fields, so the fold predicate is defeq to the constraint), prepends it to the matching list, and re-witnesses the Product. nnrat/farkas-partition-list- necessary is the whole partition -- the last piece before the layer recursion. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-partition-rowmath.rational.nnrat.farkas-reduce-listmath.rational.nnrat.farkas-elim-affine-listmath.rational.nnrat.farkas-elim-affine-list-lower

nnrat/farkas-partition-list-necessary :
  (rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))) (w : ℚ≥0)
  (reduced : nnrat/farkas-reduced-conditions rows w)
  → proposition/existence (Product) (fun pr => proposition/conjunction (nnrat/farkas-lowers-satisfied (first pr) w) (nnrat/farkas-elim-affine-rows-satisfied (second pr) w))
  where Product := data/Product (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (data/Product ℚ≥0 (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 second := product/second (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))