Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-reduced-list-satisfied

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

Farkas elimination REDUCTION CORRECTNESS (the SUFFICIENCY direction): nnrat/farkas-reduced-list-satisfied : forall rows w, farkas-reduced-conditions rows w -> farkas-both-sides-rows-satisfied rows w The existing forward theorem (reduce-list-necessary) proves satisfaction => reduced (reduced conditions are NECESSARY). This proves the converse: the reduced conditions are SUFFICIENT for the original both-sides system to be satisfied at w. Together they give the equivalence that makes the reduced system a faithful stand-in for the source. SCOPE (kept honest): this is REDUCTION CORRECTNESS, NOT partition provenance. Its conclusion is about the SOURCE rows (row-both-sides per row); there is no existential output partition here, so it is non-vacuous by construction -- a tautology-fill has nothing to attach to, and proving row-both-sides for every row REQUIRES the per-row reduced disjunction (the premise), so a premise-ignoring proof is impossible (negative control: the source singleton (0,0,1,0) is unsatisfiable). It does NOT relate the ∃(l,u) partition covering to the input rows; that partition-provenance question remains separate and open. Adding this as a conjunct to ∃(l,u),sat would still admit tautology outputs on a feasible source -- so it is reported on its own, not as the covering fix. Proof: List.rec on rows. nil -> truth. cons head tail -> split the premise into (row-reduced head w) and (reduced-conditions tail w); the IH on the tail gives (both-sides-satisfied tail w); use-disjunction on (row-reduced head w) feeds reverse lemmas -- farkas-lower-to-both-sides (from a+d~b and p<=d*w+q) and farkas-upper-to-both-sides (from b+d~a and d*w+p<=q) -- to reconstruct (row-both-sides head w); conjoin. Direction-neutral (a standalone theorem; does not rewire the covered chain or the Feasible predicate). Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-row-reconstructionmath.rational.nnrat.farkas-reduce-list

nnrat/farkas-reduced-list-satisfied :
  (rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))) (w : ℚ≥0)
  (x₁ : nnrat/farkas-reduced-conditions rows w)
  → nnrat/farkas-both-sides-rows-satisfied rows w