Reference · Non-negative rationals

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

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

Piece 1 of the n-variable capstone: the bridge-mapping -- map the structured bridge over a list of cross rows. Each structured cross row bundles the cross-product parameters (w_lo, a_hi, a_lo, b_hi) with the affine block structure (c_hi, d_hi, c_lo, d_lo) -- a Product of two 4-tuples. Given the cross condition holds at w for every row (nnrat/farkas-bridge-cross-holds), the corresponding both-sides row A*w+P<=B*w+Q holds for every row (nnrat/farkas-bridge-both-sides-hold), by mapping the single-row bridge (nnrat/farkas-cross-to-both-sides) over the list with List.rec. This is the whole structured cross system recognized as a both-sides system -- the mapped form of the eliminate-round's `link`. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-cross-bridge

nnrat/farkas-bridge-cross-holds :
  (x₁ : List (data/Product (Product) (Product))) (x₂ : ℚ≥0)
  → Prop
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))

nnrat/farkas-bridge-both-sides-hold :
  (x₁ : List (data/Product (Product) (Product))) (x₂ : ℚ≥0)
  → Prop
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))

nnrat/farkas-bridge-list-necessary :
  (rows : List (data/Product (Product) (Product))) (w : ℚ≥0)
  (crosses : nnrat/farkas-bridge-cross-holds rows w)
  → nnrat/farkas-bridge-both-sides-hold rows w
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))