Reference · Non-negative rationals

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

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

Piece (ii) recursion step: one full elimination round yields a feasible reduced lower/upper system. Composes the two big theorems of the round: eliminate a variable from a list of structured cross rows (nnrat/farkas-eliminate-structured gives the reduced disjunction system) and partition that into a lower-row list and an upper-row list (nnrat/farkas-partition-list-necessary). The result: cross conditions hold at w -> EXISTS (lowers, uppers) with brick 5b's lower fold and brick 4's upper fold both holding at w. This is the step the variable-count induction folds: each round consumes a structured cross system and produces a feasible (lower, upper) system in one fewer variable. The output folds are exactly the shape brick 6's cross-product consumes, so successive rounds chain. The full induction additionally needs the unified representation that carries each row's block structure across all remaining variables (so the next round's cross rows are again structured); this step is that recursion's proved core. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-reduce-alignmath.rational.nnrat.farkas-partition-list

nnrat/farkas-recursion-step :
  (rows : List (data/Product (Product₃) (Product₃))) (w : ℚ≥0)
  (crosses : nnrat/farkas-bridge-cross-holds rows w)
  → proposition/existence (Product) (fun pr => proposition/conjunction (nnrat/farkas-lowers-satisfied (first pr) w) (nnrat/farkas-elim-affine-rows-satisfied (second pr) w))
  where Product := data/Product (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  where Product₃ := data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))
  where first := product/first (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))
  where second := product/second (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))