Reference · Signed rationals

rainbow.math.rational.signed.decide-reflexive

Signed rationalssrc/rainbow/math/rational/signed/decide_reflexive.clj0 definitions, 3 theorems

Decision-level reflexivity for exact rational order. Order reflexivity alone does not determine which Boolean branch an executable selector takes on a tie. These theorems close that operational gap from the unary natural comparator through nnrat cross multiplication to signed cross sums: comparing a value with itself computes to true for every value, not merely for concrete numerals. Native and axiom-free on D63.

Depends onmath.rational.signed.decide-order

nat/decide-at-most-reflexive-true :
  (value : ℕ)
  → nat/decide-at-most value value = data/true

nnrat/decide-at-most-reflexive-true :
  (value : ℚ≥0)
  → audit/decide-nnrat-at-most value value = data/true

signed/decide-at-most-reflexive-true :
  (value : ℚ)
  → signed/decide-at-most value value = data/true