Reference
Binary numerals
2 modules in src/rainbow/math/rational/binary/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| math.rational.binary.rational-order | 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`. | 0 |
| math.rational.binary.signed-order | 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. | 0 |