Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-eliminate-all

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

The over-variable recursion: iterate one elimination round over the variable count. Every round reduces the number of variables by one: from the proved pieces, a feasible constraint system in k+1 variables yields a feasible system in k variables (cross-vectors-all-reduced produces the reduced system; head-split + the both-sides reduction + the dependent partition turn it into the next round's lower/upper constraints -- exactly what recursion-step does at the affine-row level). This is the induction that folds that step: nnrat/farkas-eliminate-all takes a variable count n, a feasibility predicate Feasible : Nat -> Prop, and a step (Feasible (k+1) -> Feasible k for every k), and concludes Feasible 0 from Feasible n -- eliminate all n variables, leaving the condition on the objective value alone. Proved by Nat.rec on n: base is the identity Feasible 0 -> Feasible 0; the successor applies the step then the induction hypothesis. The concrete Feasible and step (built from the round + partition machinery) instantiate this to the n-variable LP feasibility induction; the base case Feasible 0 is the objective bound, and the accumulated witnesses across the steps are the dual (piece iii). Native proof data, axiom-free.

nnrat/farkas-eliminate-all :
  (feasible : ℕ → Prop) (step : ∀ (k : ℕ), feasible (data/succ k) → feasible k) (n : ℕ)
  (init : feasible n)
  → feasible 0