Reference · Signed rationals

rainbow.math.rational.signed.decide-equivalence

Signed rationalssrc/rainbow/math/rational/signed/decide_equivalence.clj1 definitions, 1 theorems

A computable, sound equality test for signed rationals. Signed rationals are Grothendieck pairs and their mathematical equality is `signed/equivalent`, not structural equality of the pairs. Consequently a certificate generator must compare values in both order directions: signed/decide-equivalent a b = decide(a <= b) AND decide(b <= a) `signed/decide-equivalent-true-sound` turns a successful computation into the equivalence proof expected by optimality gaps and reported objective values. The proof projects both successful comparisons from Boolean conjunction, applies the signed-order decision soundness theorem twice, and closes with antisymmetry up to signed equivalence. This deliberately accepts different representations of the same rational (for example 1/2 and 2/4), while the kernel rejects a true-result witness for unequal values. Native and axiom-free on D63.

Depends onmath.rational.signed.limit-uniquenessmath.logic.boolean-andmath.rational.signed.decide-order

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

signed/decide-equivalent-true-sound :
  (left right : ℚ)
  (decided : signed/decide-equivalent left right = data/true)
  → left = right