Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-vector-round

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

The unified representation, one closed round: a feasible coefficient-vector system in k+1 variables yields a feasible affine system in k variables. This composes the whole coefficient-vector round from its proved pieces. Represent the system as next-variable constraints (coeff,(bound,(a2,rest))) -- x1 the variable eliminated this round, x2 the next -- mapped to the round's list form at x2 (farkas-adapter-map-uppers). Given the lower and upper constraints all HOLD at x1 (the k+1 system is feasible at this slice): farkas-cross-vectors-all-reduced : the pairwise reduced both-sides vector conditions hold (eliminate x1); farkas-vector-adapter-bilist : those become all-input-rows of the concatenated per-lower descriptor lists (nested fold -> flat fold); farkas-vector-partition-fold : that becomes farkas-reduced-conditions of the packed both-sides data list; farkas-partition-list-necessary : that yields EXISTS (lower-affine-list, upper-affine-list) both satisfied at x2. nnrat/farkas-vector-round is that four-step composition: the k+1 system's feasibility at x1 produces a feasible reduced affine (lower,upper) system at x2 -- one Fourier-Motzkin round on the coefficient-vector representation, end to end, axiom-free. The remaining capstone re-presents that affine output as coefficient vectors (unit-column) so the next round consumes it, wires this round into farkas-eliminate-all as the concrete step, and reads the dual off the accumulated witnesses. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-vector-adapter-bilistmath.rational.nnrat.farkas-partition-list

nnrat/farkas-vector-round :
  (lowers uppers : List (Product₃)) (x1 x2 : ℚ≥0)
  (lh : nnrat/farkas-cross-vectors-lowers-hold (uppers) x1)
  (uh : nnrat/farkas-cross-vectors-uppers-hold (uppers₅) x1)
  → proposition/existence (Product) (fun pr => proposition/conjunction (nnrat/farkas-lowers-satisfied (first pr) x2) (nnrat/farkas-elim-affine-rows-satisfied (second pr) x2))
  where Product := data/Product (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  where Product₃ := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0))))
  where first := product/first (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  where second := product/second (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  where uppers := nnrat/farkas-adapter-map-uppers lowers x2
  where uppers₅ := nnrat/farkas-adapter-map-uppers uppers x2