Reference · Binary numerals

rainbow.math.rational.binary.signed-order

Binary numeralssrc/rainbow/math/rational/binary/signed_order.clj4 definitions, 0 theorems

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

The SIGNED bridge: the checker's actual hot decision `signed/decide-at-most` on the Bin layer, proved to agree with -- and to entail the soundness of -- the trusted signed order. `signed/decide-at-most` is `reducible` to the audit decision on two nnrat SUMS of the signed parts: signed/decide-at-most a b = audit/decide-nnrat-at-most (pos a + neg b) (pos b + neg a) and `signed/at-most a b` reduces to `nnrat/at-most` of the same two sums. So the signed-level facts are thin instances of the brick-5b nnrat-level lemmas with l := (pos a + neg b) and r := (pos b + neg a): no new arithmetic, the defeq of the reducible signed definitions does the work. This is what a Bin-native checker (5c) invokes directly: bin/decide-signed-sound : decide=true -> signed/at-most a b bin/decide-signed-false-reverse : decide=false -> signed/at-most b a bin/decide-signed-matches : the Bin decision equals signed/decide-at-most a b each taking Bin representations of the two cross-SUMS' num/den. And the capstone bin/decide-signed-sound-from-parts CONSTRUCTS those cross-sums on Bin from the four signed parts (num/den of pos a, neg a, pos b, neg b) via bin-add/bin-multiply -- using the brick-5b construction theorems bin/to-nat-rat-add-num and -den (nnrat/add's num/den reduce definitionally to the cross forms, the make-predecessor convention cancelling) -- so decide=true on the fully-Bin decision entails signed/at-most a b with NO unary Nat of the operands' magnitude ever built. That is the single lemma a Bin-native checker (5c) invokes. ADDITIVE: installs into a bin-rational-order-extended environment; trusted checker untouched. Reuses bin/decide-rat-matches-audit, bin/decide-rat-sound, bin/decide-rat-false-reverse, bin/to-nat-rat-add-num, bin/to-nat-rat-add-den.

bin/decide-signed-matches :
  (a b : ℚ) (nf df nb db : data/Bin)
  (hnf : bin/to-nat nf = nnrat/numerator (signed/positive a + signed/negative b))
  (hdf : bin/to-nat df = nnrat/denominator (signed/positive a + signed/negative b))
  (hnb : bin/to-nat nb = nnrat/numerator (signed/positive b + signed/negative a))
  (hdb : bin/to-nat db = nnrat/denominator (signed/positive b + signed/negative a))
  → bin/decide-rat-at-most nf df nb db = signed/decide-at-most a b

bin/decide-signed-sound :
  (a b : ℚ) (nf df nb db : data/Bin)
  (hnf : bin/to-nat nf = nnrat/numerator (signed/positive a + signed/negative b))
  (hdf : bin/to-nat df = nnrat/denominator (signed/positive a + signed/negative b))
  (hnb : bin/to-nat nb = nnrat/numerator (signed/positive b + signed/negative a))
  (hdb : bin/to-nat db = nnrat/denominator (signed/positive b + signed/negative a))
  (h : bin/decide-rat-at-most nf df nb db = data/true)
  → a ≤ b

bin/decide-signed-false-reverse :
  (a b : ℚ) (nf df nb db : data/Bin)
  (hnf : bin/to-nat nf = nnrat/numerator (signed/positive a + signed/negative b))
  (hdf : bin/to-nat df = nnrat/denominator (signed/positive a + signed/negative b))
  (hnb : bin/to-nat nb = nnrat/numerator (signed/positive b + signed/negative a))
  (hdb : bin/to-nat db = nnrat/denominator (signed/positive b + signed/negative a))
  (h : bin/decide-rat-at-most nf df nb db = data/false)
  → b ≤ a

bin/decide-signed-sound-from-parts :
  (a b : ℚ) (pna pda nna nda pnb pdb nnb ndb : data/Bin)
  (hpna : bin/to-nat pna = nnrat/numerator (signed/positive a))
  (hpda : bin/to-nat pda = nnrat/denominator (signed/positive a))
  (hnna : bin/to-nat nna = nnrat/numerator (signed/negative a))
  (hnda : bin/to-nat nda = nnrat/denominator (signed/negative a))
  (hpnb : bin/to-nat pnb = nnrat/numerator (signed/positive b))
  (hpdb : bin/to-nat pdb = nnrat/denominator (signed/positive b))
  (hnnb : bin/to-nat nnb = nnrat/numerator (signed/negative b))
  (hndb : bin/to-nat ndb = nnrat/denominator (signed/negative b))
  (h : bin/decide-rat-at-most (add₁) (bin/bin-multiply pda ndb) (add) (bin/bin-multiply pdb nda) = data/true)
  → a ≤ b
  where add := bin/bin-add (bin/bin-multiply pnb nda) (bin/bin-multiply nna pdb)
  where add₁ := bin/bin-add (bin/bin-multiply pna ndb) (bin/bin-multiply nnb pda)