Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-elim

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_elim.clj3 definitions, 3 theorems

A bounded first Fourier--Motzkin milestone over exact nonnegative rationals. This module represents a normalized finite one-variable constraint system with two lower bounds and two upper bounds as proof data: l1 <= v, l2 <= v, v <= u1, v <= u2. Eliminating v leaves the single lattice inequality max(l1,l2) <= min(u1,u2), equivalent to the four pairwise lower/upper comparisons. The main theorem proves, constructively and in both directions, that the reduced proposition is equivalent to existence of a value satisfying the original system. In the extension direction the witness is max(l1,l2); reduced feasibility and the min/max lattice laws place it below both upper bounds. Scope: this is the fixed two-lower/two-upper normalized core, rather than list- sized coefficient-bearing inequalities. The next step is list induction that folds lower bounds with max and upper bounds with min, followed by normalization of nonzero target-variable coefficients into these bound predicates. Native and axiom-free.

Depends onmath.rational.nnrat.minmax

nnrat/farkas-elim-two-lower-two-upper-system :
  (x₁ x₂ x₃ x₄ x₅ : ℚ≥0)
  → Prop

nnrat/farkas-elim-two-lower-two-upper-reduced :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → Prop

nnrat/farkas-elim-two-lower-two-upper-solvable :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → Prop

nnrat/farkas-elim-two-lower-two-upper-extends :
  (l1 l2 u1 u2 : ℚ≥0)
  (reduced-feasible : nnrat/farkas-elim-two-lower-two-upper-reduced l1 l2 u1 u2)
  → nnrat/farkas-elim-two-lower-two-upper-solvable l1 l2 u1 u2

nnrat/farkas-elim-two-lower-two-upper-projects :
  (l1 l2 u1 u2 : ℚ≥0)
  (solution : nnrat/farkas-elim-two-lower-two-upper-solvable l1 l2 u1 u2)
  → nnrat/farkas-elim-two-lower-two-upper-reduced l1 l2 u1 u2

nnrat/farkas-elim-two-lower-two-upper-solvable-iff :
  (l1 l2 u1 u2 : ℚ≥0)
  → proposition/conjunction (reduced → solvable) (solvable → reduced)
  where reduced := nnrat/farkas-elim-two-lower-two-upper-reduced l1 l2 u1 u2
  where solvable := nnrat/farkas-elim-two-lower-two-upper-solvable l1 l2 u1 u2