Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-vector-unit-repr-length

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

Length preservation of the unit-column re-presentation map (support for the covered step migration). farkas-vector-unit-repr maps an affine-row list to a next-variable-constraint list, one output entry per input entry. So it preserves length: length(farkas-vector-unit-repr rows) = length(rows). The covered step needs this to carry the covering conjunct from the round's affine lists (length l + length u = length(packed rows)) onto the re-presented nvc lists. Proof: List.rec on rows -- nil is reflexivity (both 0), cons is one succ-congruence (repr's cons and length's cons both prepend one). Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-vector-unit-column

nnrat/farkas-vector-unit-repr-length :
  (rows : List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  → list/length (Product) (nnrat/farkas-vector-unit-repr rows) = list/length (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)) rows
  where Product := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0))))