Reference · Non-negative rationals

rainbow.math.rational.nnrat.farkas-alternative

Non-negative rationalssrc/rainbow/math/rational/nnrat/farkas_alternative.clj0 definitions, 12 theorems

Constructive Farkas alternative for arbitrary finite nnrat elimination chains. The executable cross-product comparison decides each scalar order atom. Its decisions are lifted through the upper-bound lists and the finite elimination layers, making the collapsed Fourier--Motzkin condition decidable. Transport through `farkas-elim-chain-solvable-iff` then gives the named alternative: every chain is either solvable or provably not solvable. The negative branch is a checkable Farkas certificate: a refutation of the collapsed reduced condition. All declarations are native proof data and axiom-free.

Depends onmath.rational.nnrat.farkas-elim-chainmath.rational.nnrat.order-equivalence

nat/at-most-decision-complete :
  (left right : ℕ)
  (ordered : left ≤ right)
  → nat/decide-at-most left right = data/true

nnrat/at-most-decidable :
  (left right : ℚ≥0)
  → proposition/disjunction (left ≤ right) (left ≤ right → proposition/falsity)

nnrat/farkas-upper-rest-decidable :
  (urest : List ℚ≥0) (value : ℚ≥0)
  → proposition/disjunction (data/List.rec ℚ≥0 (fun x₂₃ => Prop) proposition/truth (fun upper => fun x₂₄ => fun ih => proposition/conjunction (value ≤ upper) ih) urest) (data/List.rec ℚ≥0 (fun x₃₁ => Prop) proposition/truth (fun upper => fun x₃₂ => fun ih => proposition/conjunction (value ≤ upper) ih) urest → proposition/falsity)

nnrat/le-all-decidable :
  (u0 : ℚ≥0) (urest : List ℚ≥0) (value : ℚ≥0)
  → proposition/disjunction (nnrat/le-all u0 urest value) (nnrat/le-all u0 urest value → proposition/falsity)

nnrat/farkas-elim-list-reduced-decidable :
  (lowers : List ℚ≥0) (u0 : ℚ≥0) (urest : List ℚ≥0)
  → proposition/disjunction (reduced) (reduced → proposition/falsity)
  where reduced := nnrat/farkas-elim-list-reduced lowers u0 urest

nnrat/farkas-elim-chain-feasible-decidable :
  (layers : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0))))
  → proposition/disjunction (nnrat/farkas-elim-chain-feasible layers) (nnrat/farkas-elim-chain-feasible layers → proposition/falsity)

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

nnrat/farkas-elim-chain-infeasibility-certificate :
  (layers : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0))))
  (terminal-lowers : List ℚ≥0) (terminal-u0 : ℚ≥0) (terminal-urest : List ℚ≥0)
  (not-reduced : nnrat/farkas-elim-chain-reduced layers terminal-lowers terminal-u0 terminal-urest → proposition/falsity)
  (x₁ : nnrat/farkas-elim-chain-solvable layers terminal-lowers terminal-u0 terminal-urest)
  → proposition/falsity

nnrat/farkas-elim-chain-solvable-or-not :
  (layers : List (data/Product (List ℚ≥0) (data/Product ℚ≥0 (List ℚ≥0))))
  (terminal-lowers : List ℚ≥0) (terminal-u0 : ℚ≥0) (terminal-urest : List ℚ≥0)
  → proposition/disjunction (solvable) (solvable → proposition/falsity)
  where solvable := nnrat/farkas-elim-chain-solvable layers terminal-lowers terminal-u0 terminal-urest

nnrat/farkas-elim-chain-zero-instance-solvable :
  → nnrat/farkas-elim-chain-solvable [] [] 0 []

nnrat/farkas-elim-chain-unit-zero-instance-not-reduced :
  (x₁ : nnrat/farkas-elim-chain-reduced [] [1] 0 [])
  → proposition/falsity

nnrat/farkas-elim-chain-unit-zero-instance-not-solvable :
  (x₁ : nnrat/farkas-elim-chain-solvable [] [1] 0 [])
  → proposition/falsity