Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-vector-unit-column

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

The unified representation, unit-column re-presentation : re-present a round's affine output rows as next-variable coefficient constraints, so the round's output feeds its own input and successive rounds chain. nnrat/farkas-vector-round outputs affine rows in the just-partitioned variable x2: a lower row (a,(s,w)) satisfied at x2 means w <= a*x2 + s, an upper row (a,(s,b)) means a*x2 + s <= b (the constant s already folds in the remaining variables at the witness). The next round consumes next-variable constraints (coeff,(bound,(a2,rest))) whose hold-at form is bound <= eval(cons(coeff,x2) tail) (lower) / eval(...) <= bound (upper). The bridge is a UNIT COLUMN: carry the constant s as the coefficient of a distinguished unit variable (value nnrat/one). Re-presenting (a,(s,x)) as the next-variable constraint (a,(x,(s,nil))) and mapping it to the round's list form at the unit value (farkas-adapter-map-uppers ... one) gives the tail cons((s,one),nil), whose eval is s*1 + 0 ~ s. So lower: w <= a*x2 + s ==> w <= eval(cons(a,x2) cons((s,one),nil)) upper: a*x2 + s <= b ==> eval(cons(a,x2) cons((s,one),nil)) <= b transporting each coupling across s ~ s*1 + 0 (multiply-one-right + add-zero-right). nnrat/farkas-vector-unit-column-lower and -upper fold this over the affine row lists: a satisfied affine system re-presents as a held next-variable system. This is a satisfaction-preserving representation bridge. The constant s already contains evaluated deeper-variable terms; the bridge does not restore those columns. The current recursion's Feasible predicate ignores its variable-count argument, and the round's existential output lacks source-row provenance. General n-variable elimination and dual extraction therefore remain unproved by this chain. Native proof data, axiom-free. See the design notes.

Depends onmath.rational.nnrat.farkas-vector-adapter-bilistmath.rational.nnrat.farkas-elim-affine-listmath.rational.nnrat.farkas-elim-affine-list-lowermath.rational.nnrat.identities

nnrat/farkas-vector-unit-repr :
  (x₁ : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  → List (data/Product ℚ≥0 (Product))
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0)))

nnrat/farkas-vector-unit-column-lower :
  (rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (x2 : ℚ≥0)
  (h : nnrat/farkas-lowers-satisfied rows x2)
  → nnrat/farkas-cross-vectors-lowers-hold (uppers) x2
  where uppers := nnrat/farkas-adapter-map-uppers (nnrat/farkas-vector-unit-repr rows) 1

nnrat/farkas-vector-unit-column-upper :
  (rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (x2 : ℚ≥0)
  (h : nnrat/farkas-elim-affine-rows-satisfied rows x2)
  → nnrat/farkas-cross-vectors-uppers-hold (uppers) x2
  where uppers := nnrat/farkas-adapter-map-uppers (nnrat/farkas-vector-unit-repr rows) 1