Reference · Non-negative rationals

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

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

The vacuity FIX for the partition keystone: farkas-partition-list-necessary strengthened with a COVERING conjunct that ties the output partition to the input, killing the empty witness. farkas-partition-list-necessary concludes EXISTS (lower,upper), lowers-sat /\ uppers-sat -- which the EMPTY pair satisfies (a fold over nil is truth), so it is vacuous. The partition is proof-dependent (partition-row classifies each row by use-disjunction), so an explicit-output rewrite is unavailable; the fix keeps the existential and adds length(lower) + length(upper) = length(rows) which the empty pair fails for non-empty rows (0 =/= length(rows)). This module proves the strengthened theorem nnrat/farkas-partition-list-covered by the same List.rec as the original, additionally threading the length equation: nil is reflexivity (0+0 = 0), the lower cons is one succ-congruence (both sides reduce to succ(..) definitionally), the upper cons is a short transitive chain via nat/add-commutative (a + succ b is not definitional; succ b + a is). Built as a NEW theorem so the existing consumers are not disturbed; migrating them is a follow-on. The covering conjunct's non-vacuity is independently checked in nnrat_farkas_partition_covering_design_test. 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-covered :
  (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 (proposition/conjunction (nnrat/farkas-lowers-satisfied (first pr) w) (nnrat/farkas-elim-affine-rows-satisfied (second pr) w)) (algebra/nat-add (list/length (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)) (first pr)) (list/length (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)) (second pr)) = length))
  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 length := list/length (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) rows
  where second := product/second (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))