Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-elim-chain

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_elim_chain.clj6 definitions, 6 theorems

Arbitrary finite chains of constructive nnrat Fourier--Motzkin steps. A layer stores constant lower bounds and a non-empty upper family for one eliminated variable. Layers are ordered from the variable nearest the final survivor outwards. The open system nests one witness per layer, with every layer variable bounded above by its survivor. Folding from the tail transfers each `max-lb` onto the next variable. A final list elimination then quantifies the survivor, so `farkas-elim-chain-solvable-iff` decides chains of every finite length. All definitions and proofs are native proof data and axiom-free.

Depends onmath.rational.nnrat.farkas-elim-coupled

nnrat/farkas-elim-chain-lower :
  (x₁ : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0))))
  → ℚ≥0

nnrat/farkas-elim-chain-feasible :
  (x₁ : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0))))
  → Prop

nnrat/farkas-elim-chain-open-reduced :
  (x₁ : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0)))) (x₂ : ℚ≥0)
  → Prop

nnrat/farkas-elim-chain-open-solvable :
  (x₁ : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0)))) (x₂ : ℚ≥0)
  → Prop

nnrat/farkas-elim-chain-reduced :
  (x₁ : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0)))) (x₂ : List ℚ≥0)
  (x₃ : ℚ≥0) (x₄ : List ℚ≥0)
  → Prop

nnrat/farkas-elim-chain-solvable :
  (x₁ : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0)))) (x₂ : List ℚ≥0)
  (x₃ : ℚ≥0) (x₄ : List ℚ≥0)
  → Prop

nnrat/farkas-elim-chain-open-extends :
  (layers : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0))))
  (survivor : ℚ≥0)
  (reduced-feasible : nnrat/farkas-elim-chain-open-reduced layers survivor)
  → nnrat/farkas-elim-chain-open-solvable layers survivor

nnrat/farkas-elim-chain-open-projects :
  (layers : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0))))
  (survivor : ℚ≥0) (solution : nnrat/farkas-elim-chain-open-solvable layers survivor)
  → nnrat/farkas-elim-chain-open-reduced layers survivor

nnrat/farkas-elim-chain-open-solvable-iff :
  (layers : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0))))
  (survivor : ℚ≥0)
  → proposition/conjunction (reduced → solvable) (solvable → reduced)
  where reduced := nnrat/farkas-elim-chain-open-reduced layers survivor
  where solvable := nnrat/farkas-elim-chain-open-solvable layers survivor

nnrat/farkas-elim-chain-extends :
  (layers : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0))))
  (terminal-lowers : List ℚ≥0) (terminal-u0 : ℚ≥0) (terminal-urest : List ℚ≥0)
  (reduced-feasible : nnrat/farkas-elim-chain-reduced layers terminal-lowers terminal-u0 terminal-urest)
  → nnrat/farkas-elim-chain-solvable layers terminal-lowers terminal-u0 terminal-urest

nnrat/farkas-elim-chain-projects :
  (layers : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0))))
  (terminal-lowers : List ℚ≥0) (terminal-u0 : ℚ≥0) (terminal-urest : List ℚ≥0)
  (solution : nnrat/farkas-elim-chain-solvable layers terminal-lowers terminal-u0 terminal-urest)
  → nnrat/farkas-elim-chain-reduced layers terminal-lowers terminal-u0 terminal-urest

nnrat/farkas-elim-chain-solvable-iff :
  (layers : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0))))
  (terminal-lowers : List ℚ≥0) (terminal-u0 : ℚ≥0) (terminal-urest : List ℚ≥0)
  → proposition/conjunction (reduced → solvable) (solvable → reduced)
  where reduced := nnrat/farkas-elim-chain-reduced layers terminal-lowers terminal-u0 terminal-urest
  where solvable := nnrat/farkas-elim-chain-solvable layers terminal-lowers terminal-u0 terminal-urest