Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-cross-bridge

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

Piece 1 core of the n-variable capstone: the structured bridge recognizing a cross condition as a both-sides row. brick 6's cross-product core emits cross conditions with OPAQUE survivor blocks; the recursive reduction consumes STRUCTURED both-sides rows A*v+P <= B*v+Q. This bridge discharges that seam for the general AFFINE block case: when the eliminated variable's blocks are affine in the next variable w, s_hi = c_hi*w + d_hi and s_lo = c_lo*w + d_lo, a single cross condition w_lo*a_hi + s_hi*a_lo <= b_hi*a_lo + s_lo*a_hi IS the both-sides row A*w + P <= B*w + Q with A = c_hi*a_lo, P = w_lo*a_hi + d_hi*a_lo, B = c_lo*a_hi, Q = b_hi*a_lo + d_lo*a_hi. nnrat/farkas-cross-to-both-sides proves the cross condition implies that both-sides row (necessary direction). Each side is realigned up to nnrat equivalence -- distribute the block (multiply-distributes-add-right), fold the w-coefficient (multiply-swap-right), lift the w-term to the front (add-swap-right) -- and transported by at-most-respects-equivalence. Mapping this over the bilist cross-condition structure is what discharges the eliminate-round's `link`, turning the elimination round into a closed step of the variable-count induction. Native proof data, axiom-free.

Depends onmath.rational.nnrat.add-monotonemath.rational.nnrat.additive-reassociationmath.rational.nnrat.distribute-rightmath.rational.nnrat.multiply-commutemath.rational.nnrat.product-reassociation

nnrat/farkas-cross-to-both-sides :
  (w-lo a-hi a-lo b-hi c-hi d-hi c-lo d-lo w : ℚ≥0)
  (cross : w-lo · a-hi + (c-hi · w + d-hi) · a-lo ≤ b-hi · a-lo + (c-lo · w + d-lo) · a-hi)
  → c-hi · a-lo · w + (w-lo · a-hi + d-hi · a-lo) ≤ c-lo · a-hi · w + (b-hi · a-lo + d-lo · a-hi)