Reference · Signed rationals

rainbow.math.rational.signed.pointwise-order

Signed rationalssrc/rainbow/math/rational/signed/pointwise_order.clj1 definitions, 4 theorems

Pointwise order over the indices a problem actually has. The parametric LP theorems quantify their feasibility hypotheses over the whole index TYPE -- `forall i : A, ...`. That is the right statement for a theorem and the wrong one for an instance. A real program has data for the rows in its row list and for nothing else, so on an index type like `data/Nat` the hypothesis is not merely inconvenient to discharge, it is FALSE: there is no eighth constraint to satisfy. Only a finite index type such as `data/Bool` escapes that, which caps a checker at instances whose size was fixed when the theorem was written. `signed/all-at-most` fixes the quantifier to the list: all-at-most f g nil = truth all-at-most f g (h :: t) = (f h <= g h) AND all-at-most f g t and `signed/map-sum-monotone-on` is the monotonicity a finite sum actually needs -- termwise domination ON THE SUMMED INDICES lifts to the sum. The existing `signed/map-sum-monotone` is the special case where domination happens to hold everywhere. For an instance of any size the hypothesis is then built by folding one decided comparison per row, which a generator emits in a loop. Nothing here is quadratic in the instance and nothing is fixed at theorem-writing time. Native and axiom-free on D63; chains the signed finite-sum order laws.

Depends onmath.rational.signed.list-sum

signed/all-at-most.{u} :
  (A : Type u) (f g : A → ℚ) (x₁ : List A)
  → Prop

signed/all-at-most-empty.{u} :
  (A : Type u) (f g : A → ℚ)
  → ∀ i ∈ [], f i ≤ g i

signed/all-at-most-cons.{u} :
  (A : Type u) (f g : A → ℚ) (head : A) (tail : List A)
  (here : f head ≤ g head)
  (rest : ∀ i ∈ tail, f i ≤ g i)
  → ∀ i ∈ data/cons A head tail, f i ≤ g i

signed/all-at-most-combine.{u} :
  (A : Type u) (f g p q r s : A → ℚ) (xs : List A)
  (step : ∀ (x : A), ∀ (first : f x ≤ g x), ∀ (second : p x ≤ q x), r x ≤ s x)
  (first : ∀ i ∈ xs, f i ≤ g i)
  (second : ∀ i ∈ xs, p i ≤ q i)
  → ∀ i ∈ xs, r i ≤ s i

signed/map-sum-monotone-on.{u} :
  (A : Type u) (f g : A → ℚ) (xs : List A)
  (dominated : ∀ i ∈ xs, f i ≤ g i)
  → Σ j∈xs, f j ≤ Σ j∈xs, g j