Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-row-reconstruction

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_row_reconstruction.clj0 definitions, 2 theorems

Reconstruct a source inequality from its reduced affine row and coefficient equation. These are the converse directions to nnrat-farkas-both-sides: a+d ~ b, p <= d*v+q ==> a*v+p <= b*v+q b+d ~ a, d*v+p <= q ==> a*v+p <= b*v+q. Together with the existing forward theorems they establish row satisfaction equivalence at every v. The difference equation is essential provenance; cardinality or a sum of constants cannot replace it. Partition completeness and the relation between whole input/output lists remain separate obligations. Native proof data, no new axioms.

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

nnrat/farkas-lower-to-both-sides :
  (a b d p q v : ℚ≥0)
  (diff : a + d = b)
  (reduced : p ≤ d · v + q)
  → a · v + p ≤ b · v + q

nnrat/farkas-upper-to-both-sides :
  (a b d p q v : ℚ≥0)
  (diff : b + d = a)
  (reduced : d · v + p ≤ q)
  → a · v + p ≤ b · v + q