Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-form-scale

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_form_scale.clj1 definitions, 1 theorems

The unified representation, brick 2 core: scaling a linear form scales its coefficient vector. The columnwise cross transform's arithmetic: crossing a lower row against an upper row multiplies one row's tail linear form by the other's head coefficient (e.g. eval(U_tail)*L_1). nnrat/farkas-form-scale-right proves eval(pairs) * c ~ eval(scale-right c pairs), where nnrat/farkas-scale-right multiplies each coefficient by c (the variables unchanged). So the cross's product terms ARE linear forms over the same tail variables with scaled coefficient vectors -- the bookkeeping that lets the reduced constraint be read as a coefficient vector over the remaining variables. Proof: List.rec over the pairs; nil by multiply-zero-left; cons by distribute-right then multiply-swap-right (fold the scalar into the coefficient) then the IH. Native proof data, axiom-free.

Depends onmath.rational.nnrat.distribute-rightmath.rational.nnrat.multiply-commutemath.rational.nnrat.product-reassociationmath.rational.nnrat.identitiesmath.rational.nnrat.farkas-linear-form

nnrat/farkas-scale-right :
  (x₁ : ℚ≥0) (x₂ : List (data/Product ℚ≥0 ℚ≥0))
  → List (data/Product ℚ≥0 ℚ≥0)

nnrat/farkas-form-scale-right :
  (c : ℚ≥0) (pairs : List (data/Product ℚ≥0 ℚ≥0))
  → nnrat/linear-form pairs · c = nnrat/linear-form (nnrat/farkas-scale-right c pairs)