Reference · Signed rationals

rainbow.math.rational.signed.decide-order

Signed rationalssrc/rainbow/math/rational/signed/decide_order.clj1 definitions, 2 theorems

A DECIDABLE signed-rational order -- the per-instance half of a certificate. The optimality theorems in `rainbow.math.rational.signed.lp-duality` are parametric: they hold for every matrix, cost vector and dual vector. Applying one to an actual customer instance means discharging its hypotheses -- primal feasibility, dual feasibility, nonnegativity -- for actual numbers. Without a decision procedure each of those inequalities needs a hand-built proof, which is why the parametric theorems, on their own, do not yet check anything. signed/decide-at-most : signed -> signed -> Bool (computable) signed/decide-at-most-true-sound : decide a b = true -> a <= b signed/decide-at-most-false-reverse : decide a b = false -> b <= a With these, a concrete inequality is discharged by REDUCTION: the decision computes to `true`, `equality/reflexive` proves that it did, and soundness turns it into the order fact the theorem wants. That is the shape a checker needs -- expensive parametric proof once, cheap arithmetic per instance. The bridge is definitional rather than earned. Signed order `a <= b` unfolds to the nnrat comparison `positive a + negative b <= positive b + negative a`, so the existing decidable nnrat order applied to those two cross sums IS the decision procedure, and the existing nnrat soundness lemmas applied to the same two terms ARE its soundness proofs. Nothing new is assumed and the trusted base is unchanged. Native and axiom-free on D63.

signed/decide-at-most :
  (x₁ x₂ : ℚ)
  → data/Bool

signed/decide-at-most-true-sound :
  (a b : ℚ)
  (decided : signed/decide-at-most a b = data/true)
  → a ≤ b

signed/decide-at-most-false-reverse :
  (a b : ℚ)
  (decided : signed/decide-at-most a b = data/false)
  → b ≤ a