Reference · Binary numerals

rainbow.math.rational.binary.rational-order

Binary numerals src/rainbow/math/rational/binary/rational_order.clj9 definitions, 0 theorems

In Rainbow 1.4.1, lein verify rainbow.math.rational.binary.rational-order fails on its own: the module uses lemmas from data.binary without listing them in its dependencies. It checks once those are installed.

Brick 5b of the binary-numeral roadmap: a Bin-NATIVE rational comparison, proved to agree with the trusted checker's rational decision `audit/decide-nnrat-at-most`. The checker decides `l <= r` for nonnegative rationals by the cross-multiplication audit/decide-nnrat-at-most l r = nat/decide-at-most (num l * den r) (num r * den l) on unary `Nat` -- which is where the magnitude ceiling bites (see memory rainbow-scaling-bridge-magnitude-wall). Here the SAME decision is expressed on `data/Bin` numerals: bin/decide-rat-at-most nl dl nr dr = bin/at-most (nl * dr) (nr * dl) (all Bin) and proved equal, through `to-nat`, to the nat-level cross-multiply decision (`bin/decide-rat-at-most-reflects`), hence to `audit/decide-nnrat-at-most` whenever the Bin fields represent the rational's num/den (`bin/decide-rat-matches-audit`). This is ADDITIVE: it installs definitions into a Bin-extended checked environment and does NOT touch the trusted checker. It is the foundation a Bin-native checker (brick 5c) would wire in. Reuses `bin/at-most-reflects` and `bin/to-nat-bin-multiply` from rainbow.data.binary.

bin/decide-rat-at-most

DefinitionSource, line 62

bin/decide-rat-at-most :
  (x₁ x₂ x₃ x₄ : data/Bin)
  → data/Bool

bin/decide-rat-at-most-reflects

DefinitionSource, line 74

bin/decide-rat-at-most-reflects :
  (nl dl nr dr : data/Bin)
  → bin/decide-rat-at-most nl dl nr dr = nat/decide-at-most (multiply) (multiply₁)
  where multiply := nat/multiply (bin/to-nat nl) (bin/to-nat dr)
  where multiply₁ := nat/multiply (bin/to-nat nr) (bin/to-nat dl)

= = equality/Eq

bin/decide-rat-matches-audit

DefinitionSource, line 99

bin/decide-rat-matches-audit :
  (l r : ℚ≥0) (nl dl nr dr : data/Bin)
  (hnl : bin/to-nat nl = nnrat/numerator l)
  (hdl : bin/to-nat dl = nnrat/denominator l)
  (hnr : bin/to-nat nr = nnrat/numerator r)
  (hdr : bin/to-nat dr = nnrat/denominator r)
  → bin/decide-rat-at-most nl dl nr dr = audit/decide-nnrat-at-most l r

= = equality/Eqℚ≥0 = nnrat/NonnegativeRational

bin/decide-rat-at-most-true-sound

DefinitionSource, line 156

bin/decide-rat-at-most-true-sound :
  (nl dl nr dr : data/Bin)
  (h : bin/decide-rat-at-most nl dl nr dr = data/true)
  → nat/multiply (bin/to-nat nl) (bin/to-nat dr) ≤ nat/multiply (bin/to-nat nr) (bin/to-nat dl)

= = equality/Eq≤ = nat/at-most

bin/decide-rat-at-most-false-reverse

DefinitionSource, line 176

bin/decide-rat-at-most-false-reverse :
  (nl dl nr dr : data/Bin)
  (h : bin/decide-rat-at-most nl dl nr dr = data/false)
  → nat/multiply (bin/to-nat nr) (bin/to-nat dl) ≤ nat/multiply (bin/to-nat nl) (bin/to-nat dr)

= = equality/Eq≤ = nat/at-most

bin/decide-rat-sound

DefinitionSource, line 205

bin/decide-rat-sound :
  (l r : ℚ≥0) (nl dl nr dr : data/Bin)
  (hnl : bin/to-nat nl = nnrat/numerator l)
  (hdl : bin/to-nat dl = nnrat/denominator l)
  (hnr : bin/to-nat nr = nnrat/numerator r)
  (hdr : bin/to-nat dr = nnrat/denominator r)
  (h : bin/decide-rat-at-most nl dl nr dr = data/true)
  → l ≤ r

= = equality/Eqℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most

bin/decide-rat-false-reverse

DefinitionSource, line 238

bin/decide-rat-false-reverse :
  (l r : ℚ≥0) (nl dl nr dr : data/Bin)
  (hnl : bin/to-nat nl = nnrat/numerator l)
  (hdl : bin/to-nat dl = nnrat/denominator l)
  (hnr : bin/to-nat nr = nnrat/numerator r)
  (hdr : bin/to-nat dr = nnrat/denominator r)
  (h : bin/decide-rat-at-most nl dl nr dr = data/false)
  → r ≤ l

= = equality/Eqℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most

bin/to-nat-rat-add-num

DefinitionSource, line 278

bin/to-nat-rat-add-num :
  (p q : ℚ≥0) (np dp nq dq : data/Bin)
  (hnp : bin/to-nat np = nnrat/numerator p)
  (hdp : bin/to-nat dp = nnrat/denominator p)
  (hnq : bin/to-nat nq = nnrat/numerator q)
  (hdq : bin/to-nat dq = nnrat/denominator q)
  → bin/to-nat (bin/bin-add (bin/bin-multiply np dq) (bin/bin-multiply nq dp)) = nnrat/numerator (p + q)

+ = nnrat/add= = equality/Eqℚ≥0 = nnrat/NonnegativeRational

bin/to-nat-rat-add-den

DefinitionSource, line 313

bin/to-nat-rat-add-den :
  (p q : ℚ≥0) (dp dq : data/Bin)
  (hdp : bin/to-nat dp = nnrat/denominator p)
  (hdq : bin/to-nat dq = nnrat/denominator q)
  → bin/to-nat (bin/bin-multiply dp dq) = nnrat/denominator (p + q)

+ = nnrat/add= = equality/Eqℚ≥0 = nnrat/NonnegativeRational