Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-vector-partition-fold

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

The unified representation, partition bridge (the fold) : collect a LIST of reduced coefficient-vector rows into the affine partition's input. The 2026-09-09 finding: farkas-partition-list-necessary is generic in the per-row (A,B,P,Q), so the coefficient-vector round bridges to it rather than re-proving a partition. nnrat/farkas-vector-partition-pack packed one reduced row; this folds that across the round's reduced rows. A reduced (lower,upper) pair is a descriptor bundling (l1, u1, b_L, b_U, a2l, a2u, rl, ru): the two x1-coefficients, the two bounds, and -- with the next variable x2 the head of each tail -- the two x2-coefficients and the two rest-vectors. nnrat/farkas-vector-partition-fold takes a list of these and a proof that each one's reduced both-sides vector row holds at x2 (all-input-rows, a conjunction fold), and produces farkas-reduced-conditions of the packed both-sides DATA list (packed-list = the per-descriptor packed rows). Proof: List.rec over the descriptors; nil is truth, each cons discharges its head via nnrat/farkas-vector-both-sides-reduce (defeq to reduce-list's row-reduced of the packed row) conjoined with the tail's fold. The packed list and this proof are exactly farkas-partition-list-necessary's two inputs, so feeding them yields the next round's affine lower/upper lists -- the round's reduction to a system in one fewer variable, on the coefficient-vector representation. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-vector-both-sides-reducemath.rational.nnrat.farkas-reduce-list

nnrat/farkas-vector-partition-input-rows :
  (x₁ : List (data/Product ℚ≥0 (Product))) (x₂ : ℚ≥0)
  → Prop
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product (List (data/Product ℚ≥0 ℚ≥0)) (List (data/Product ℚ≥0 ℚ≥0)))))))

nnrat/farkas-vector-partition-packed :
  (x₁ : List (data/Product ℚ≥0 (Product)))
  → List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product (List (data/Product ℚ≥0 ℚ≥0)) (List (data/Product ℚ≥0 ℚ≥0)))))))

nnrat/farkas-vector-partition-fold :
  (descs : List (data/Product ℚ≥0 (Product))) (x2 : ℚ≥0)
  (h : nnrat/farkas-vector-partition-input-rows descs x2)
  → nnrat/farkas-reduced-conditions (nnrat/farkas-vector-partition-packed descs) x2
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product (List (data/Product ℚ≥0 ℚ≥0)) (List (data/Product ℚ≥0 ℚ≥0)))))))