Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-linear-form

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_linear_form.clj1 definitions, 2 theorems

The unified representation, brick 1: the coefficient-vector (linear-form) constraint type and the head-split extraction. A constraint over the remaining variables is a list of (coefficient, variable) pairs; nnrat/linear-form evaluates it to sum_i c_i*x_i. The representation is closed under elimination: the head pair is the current variable's (coefficient, value) and the tail is the block over the remaining variables. nnrat/linear-form-upper-split and -lower-split expose exactly that -- an upper constraint eval(cons p tail) <= b holds iff fst(p)*snd(p) + eval(tail) <= b (and the lower analogue), because eval(cons p tail) reduces definitionally to fst(p)*snd(p) + eval(tail). So a coefficient-vector row presents as the structured affine row the elimination round consumes, with block = eval(tail) (itself affine in the next variable, its head). The columnwise cross transform over these vectors is brick 2. Native proof data, axiom-free.

nnrat/linear-form :
  (x₁ : List (data/Product ℚ≥0 ℚ≥0))
  → ℚ≥0

nnrat/linear-form-upper-split :
  (p : data/Product ℚ≥0 ℚ≥0) (tail : List (data/Product ℚ≥0 ℚ≥0)) (b : ℚ≥0)
  (h : nnrat/linear-form (data/cons (data/Product ℚ≥0 ℚ≥0) p tail) ≤ b)
  → product/first ℚ≥0 ℚ≥0 p · product/second ℚ≥0 ℚ≥0 p + nnrat/linear-form tail ≤ b

nnrat/linear-form-lower-split :
  (w : ℚ≥0) (p : data/Product ℚ≥0 ℚ≥0) (tail : List (data/Product ℚ≥0 ℚ≥0))
  (h : w ≤ nnrat/linear-form (data/cons (data/Product ℚ≥0 ℚ≥0) p tail))
  → w ≤ product/first ℚ≥0 ℚ≥0 p · product/second ℚ≥0 ℚ≥0 p + nnrat/linear-form tail