Reference · Non-negative rationals

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

Non-negative rationals src/rainbow/math/rational/nnrat/farkas_recursion_step_covered.clj0 definitions, 1 theorems

Covered recursion step (the vacuity fix, consumer migration): the affine elimination round built on the COVERING-strengthened partition keystone. farkas-recursion-step produced the vacuous goal EXISTS (l,u), sat -- inherited from farkas-partition-list-necessary. This variant, farkas-recursion-step- covered, is the identical composition but applies nnrat/farkas-partition-list-covered instead, so its conclusion carries the covering conjunct length(l)+length(u)=length(to-bs rows) and is therefore NOT empty-satisfiable. It is the first consumer migrated onto the strengthened keystone. The point of the exercise (the vacuity lesson): this proof DEPENDS on the covered keystone -- its value is exactly partition-list-covered applied to the eliminated structured rows -- so if the keystone stopped holding, this proof breaks loudly rather than silently falling back to a weaker fact. A dependency guard in the test asserts the proof value mentions farkas-partition-list- covered. Native proof data, axiom-free.

Depends onmath.rational.nnrat.farkas-reduce-align math.rational.nnrat.farkas-partition-list math.rational.nnrat.farkas-partition-covered

nnrat/farkas-recursion-step-covered

TheoremFor all inputsNo axiomsSource, line 83

nnrat/farkas-recursion-step-covered :
  (rows : List (data/Product (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))))
  (w : ℚ≥0) (crosses : nnrat/farkas-bridge-cross-holds rows w)
  → proposition/existence (Product) (fun pr => proposition/conjunction (proposition/conjunction (nnrat/farkas-lowers-satisfied (first pr) w) (nnrat/farkas-elim-affine-rows-satisfied (second pr) w)) (algebra/nat-add (list/length (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)) (first pr)) (list/length (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)) (second pr)) = length))
  where Product := data/Product (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (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 length := list/length (data/Product ℚ≥0 (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (nnrat/farkas-structured-to-both-sides rows)
  where second := product/second (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0))) (List (data/Product ℚ≥0 (data/Product ℚ≥0 ℚ≥0)))

= = equality/EqList = data/Listℚ≥0 = nnrat/NonnegativeRational