Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-reduce-align

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

Piece (i) of the n-variable capstone: the data-representation alignment that lets the elimination round close on structured cross rows. The bridge-mapping (nnrat/farkas-bridge-list-necessary) proves the both-sides conditions hold as a fold over STRUCTURED cross rows (base4 x block4); the recursive reduction (nnrat/farkas-reduce-list-necessary) consumes a fold over 4-TUPLE both-sides rows. This aligns them: nnrat/farkas-structured-to-both-sides maps each structured row to its 4-tuple (A=c_hi*a_lo, B=c_lo*a_hi, P=w_lo*a_hi+d_hi*a_lo, Q=b_hi*a_lo+d_lo*a_hi), and nnrat/farkas-reduce-align proves the bridge-mapping's fold implies the reduction's fold over the mapped list -- the per-row predicates are definitionally equal (the map's projections reduce to the fields), so a List.rec carries each head proof directly. nnrat/farkas-eliminate-structured then chains bridge-mapping -> align -> reduction: given the cross condition holds at w for every structured row, the reduced affine-row system holds. This is one full elimination round on the structured representation, with the `link` fully discharged -- the closed step the variable-count induction folds. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-bridge-listmath.rational.nnrat.farkas-reduce-list

nnrat/farkas-structured-to-both-sides :
  (x₁ : List (data/Product (Product) (Product)))
  → List (Product)
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))

nnrat/farkas-reduce-align :
  (rows : List (data/Product (Product) (Product))) (w : ℚ≥0)
  (hold : nnrat/farkas-bridge-both-sides-hold rows w)
  → nnrat/farkas-both-sides-rows-satisfied (nnrat/farkas-structured-to-both-sides rows) w
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))

nnrat/farkas-eliminate-structured :
  (rows : List (data/Product (Product) (Product))) (w : ℚ≥0)
  (crosses : nnrat/farkas-bridge-cross-holds rows w)
  → nnrat/farkas-reduced-conditions (nnrat/farkas-structured-to-both-sides rows) w
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))