Reference · Non-negative rationals

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

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

Recursive-reduction sub-brick of brick 6 (list form): map the single-row reduction over a list of both-sides cross rows. The both-sides cross system produced by eliminating a variable is a LIST of rows A_i*v + P_i <= B_i*v + Q_i (each row a Product quadruple (A,(B,(P,Q)))). nnrat/farkas-reduce-list-necessary proves: if every row holds at v (nnrat/farkas-both-sides-rows-satisfied), then every row reduces to an affine row in v (nnrat/farkas-reduced-conditions) -- a lower row when A_i<=B_i, an upper row when B_i<=A_i -- by applying the single-row reduction (nnrat/farkas-both-sides-reduce) to each via List.rec. Both predicates still describe rows evaluated at the SAME variable v. This theorem converts each both-sides row to a disjunction of affine-row conditions; it does not itself eliminate v or produce a related partition of output row lists. Eliminating a coordinate requires a separate existential projection theorem. The variable-count recursion, partition provenance and dual extraction are separate obligations. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-both-sides-reduce

nnrat/farkas-both-sides-rows-satisfied :
  (x₁ : List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))) (x₂ : ℚ≥0)
  → Prop

nnrat/farkas-reduced-conditions :
  (x₁ : List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))) (x₂ : ℚ≥0)
  → Prop

nnrat/farkas-reduce-list-necessary :
  (rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))) (v : ℚ≥0)
  (satisfied : nnrat/farkas-both-sides-rows-satisfied rows v)
  → nnrat/farkas-reduced-conditions rows v