Reference · Non-negative rationals

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

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

The unified representation, partition bridge (single row) : pack one reduced coefficient-vector row into a both-sides DATA row and discharge its reduced-conditions entry. Architectural finding (2026-09-09): the affine nnrat/farkas-partition-list-necessary is generic in the per-row (A,B,P,Q). It consumes a data list of both-sides rows (A,(B,(P,Q))) plus a proof that nnrat/farkas-reduced-conditions holds (the per-row lower/upper disjunction fold), and returns the next round's lower/upper AFFINE-row lists. So the coefficient-vector round needs only a BRIDGE that packs its reduced rows as that data and supplies that proof -- no re-proved partition. This is the bridge's single-row core. A reduced both-sides vector row (farkas-cross-vectors output, tails headed by the next variable x2) packs into the data row (AL,(AR,(P,Q))) with AL = a2u*l1, AR = a2l*u1, P = b_L*u1 + eval(scale l1 ru), Q = b_U*l1 + eval(scale u1 rl). For that packed row the projections bs-a/bs-b/bs-p/bs-q reduce definitionally to AL/AR/P/Q, so reduce-list's per-row disjunction (row-reduced) is defeq to nnrat/farkas-vector-both-sides-reduce's output. Hence farkas-reduced-conditions of the one-element packed list is just that reduction conjoined with truth. nnrat/farkas-vector-partition-pack proves it -- the defeq-carry that lets the bilist fold (the bridge proper) emit a list-bs of packed rows and its reduced-conditions proof, then hand them to the already-proved partition. Native proof data, axiom-free.

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

nnrat/farkas-vector-partition-pack :
  (l-coeff u-coeff b-l b-u a2l a2u : ℚ≥0) (rl ru : List (data/Product ℚ≥0 ℚ≥0))
  (x2 : ℚ≥0)
  (h : b-l · u-coeff + nnrat/linear-form (nnrat/farkas-scale-right l-coeff (cons)) ≤ b-u · l-coeff + nnrat/linear-form (nnrat/farkas-scale-right u-coeff (cons₂)))
  → nnrat/farkas-reduced-conditions [pair] x2
  where cons := data/cons (data/Product ℚ≥0 ℚ≥0) (data/pair ℚ≥0 ℚ≥0 a2u x2) ru
  where cons₂ := data/cons (data/Product ℚ≥0 ℚ≥0) (data/pair ℚ≥0 ℚ≥0 a2l x2) rl
  where pair := data/pair ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)) (a2u · l-coeff) (data/pair ℚ≥0 (data/Product ℚ≥0 ℚ≥0) (a2l · u-coeff) (data/pair ℚ≥0 ℚ≥0 (b-l · u-coeff + nnrat/linear-form (nnrat/farkas-scale-right l-coeff ru)) (b-u · l-coeff + nnrat/linear-form (nnrat/farkas-scale-right u-coeff rl))))