Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-vector-step

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_vector_step.clj1 definitions, 3 theorems

The unified representation, the recursion step: one closed elimination step in the held next-variable representation, and its instantiation of the over-variable recursion skeleton. farkas-vector-round eliminates a variable and yields a feasible AFFINE system; farkas-vector-unit-column-lower/-upper re-present that affine system as a HELD next-variable system (constant carried as a unit column). Composed -- unpacking the round's existential in between -- they give one step in a single representation: nnrat/farkas-vector-step : given lower/upper next-variable constraints held at x1 (tail head x2), there EXIST lower/upper next-variable constraints held at x2 (tail head the unit value). The stated output has the same held representation. Its existential lists are not related to the input lists by this type; empty lists can witness it. Wrapping the value into a closed predicate Feasible : Nat -> Prop (nnrat/farkas-vector-feasible k = EXISTS value and lower/upper next-variable lists held at that value over the unit column) makes this exactly the step the recursion skeleton folds: nnrat/farkas-vector-eliminate : Feasible n -> Feasible 0, via nnrat/farkas-eliminate-all with step = farkas-vector-step. This instantiates a recursion schema, but Feasible ignores k; the types of farkas-vector-feasible-step and farkas-vector-eliminate admit identity proofs. The theorem does not establish elimination of n coordinates from a specified input system. Symbolic survivor columns, a source-related transformation, its existential projection theorem, and separate multiplier/dual-extraction proofs remain required. The new source-row reconstruction results do not silently change this predicate or its consumers. Native proof data, axiom-free. See the design notes.

Depends onmath.rational.nnrat.farkas-vector-roundmath.rational.nnrat.farkas-vector-unit-columnmath.rational.nnrat.farkas-eliminate-all

nnrat/farkas-vector-feasible :
  (x₁ : ℕ)
  → Prop

nnrat/farkas-vector-step :
  (lowers uppers : List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0))))))
  (x1 x2 : ℚ≥0) (lh : nnrat/farkas-cross-vectors-lowers-hold (uppers) x1)
  (uh : nnrat/farkas-cross-vectors-uppers-hold (uppers₄) x1)
  → proposition/existence (Product) (fun pr => proposition/conjunction (nnrat/farkas-cross-vectors-lowers-hold (nnrat/farkas-adapter-map-uppers (first pr) 1) x2) (nnrat/farkas-cross-vectors-uppers-hold (nnrat/farkas-adapter-map-uppers (second pr) 1) x2))
  where Product := data/Product (List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0)))))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0))))))
  where first := product/first (List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0)))))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0))))))
  where second := product/second (List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0)))))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 (List (data/Product ℚ≥0 ℚ≥0))))))
  where uppers := nnrat/farkas-adapter-map-uppers lowers x2
  where uppers₄ := nnrat/farkas-adapter-map-uppers uppers x2

nnrat/farkas-vector-feasible-step :
  (k : ℕ) (fk : nnrat/farkas-vector-feasible (data/succ k))
  → nnrat/farkas-vector-feasible k

nnrat/farkas-vector-eliminate :
  (n : ℕ) (init : nnrat/farkas-vector-feasible n)
  → nnrat/farkas-vector-feasible 0