Reference
Natural numbers
29 modules in src/rainbow/math/nat/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| math.nat.add-order | Additive monotonicity building blocks for the convergence proof: a natural number is at most itself plus anything, and in particular at most its own double. | 2 |
| math.nat.at-most-add | Three one-line order facts about addition that the program-family index arithmetic keeps needing (nat/at-most a b unfolds to exists e, a + e = b; addition recurses on its LEFT argument, so `a <= a + b` is a direct witness but `a <= b + a` needs commutativity and the nested form needs associativity): nat/at-most-add-right : a <= a + b nat/at-most-add-left : a <= b + a nat/at-most-add-nested : a + b | 5 |
| math.nat.at-most-cancellation | Real-analysis bedrock (roadmap step 1): cancellation for the nat order. | 4 |
| math.nat.contraction | Natural multiplication laws needed by finite metric contraction proofs. | 10 |
| math.nat.distance | Computational natural distance and additive foreign-vocabulary bridges. | 6 |
| math.nat.distance-core | Constructive zero and identity laws for computational natural distance. | 6 |
| math.nat.distance-radius | Natural distance is the least symmetric additive radius. | 3 |
| math.nat.distributive | Left-distributivity of nat multiplication over addition: a * (b + c) = a * b + a * c for all a, b, c, the semiring law missing from nat_semiring (which has associativity, commutativity of addition, multiply-one-right, but not distributivity). | 2 |
| math.nat.divisibility | Native natural-number divisibility for arithmetic proof interfaces. | 0 |
| math.nat.divmod | Row/column of a FLAT PAIR INDEX, kernel-side, with the bounds the pair-vector families need (Floyd-Warshall's round is a block of n*n components indexed by c = col + row*n). | 8 |
| math.nat.extremal-index | LEAST AND GREATEST WITNESSES of a decidable predicate on 0..k, constructively (for the Floyd-Warshall invariant: the first and last intermediate visit of the new pivot). | 3 |
| math.nat.infinite | Axiom-free Nat constructor discrimination, list bounds, and infinitude. | 7 |
| math.nat.linear-order | Executable decision data, min/max, and three-way comparison for Nat. | 0 |
| math.nat.metric | Constructive order laws for computational natural distance. | 3 |
| math.nat.metric-separation | Constructive positivity and separation laws for computational Nat distance. | 5 |
| math.nat.monus | Truncated subtraction on Nat (monus), the missing arithmetic primitive under the signed->nnrat magnitude foundation. | 3 |
| math.nat.multiply-positive | Constructive nat positivity of a product: 0 < a -> 0 < b -> 0 < a*b (strict-below form). | 1 |
| math.nat.multiply-zero-split | nat/multiply-zero-split : a*b = 0 -> (a = 0) or (b = 0). | 1 |
| math.nat.order | Constructive monotonicity for Nat arithmetic and finite expectation. | 11 |
| math.nat.pair-index-inverse | INVERTING THE PAIR INDEX. | 4 |
| math.nat.pigeonhole | THE PIGEONHOLE PRINCIPLE ON NAT, constructively. | 3 |
| math.nat.power | Natural-number exponentiation base^exp, defined by recursion on the exponent: power b 0 = 1 power b (succ e) = b * (power b e). | 5 |
| math.nat.power-growth | Growth lemmas for nat exponentiation, on the road to the geometric-convergence modulus. | 3 |
| math.nat.ring-reflect | Definitions for proving nat semiring identities BY REFLECTION. | 0 |
| math.nat.ring-reflect-sound | Unconditional, native soundness of the nat reflection normalizer. | 8 |
| math.nat.semiring | Constructive natural semiring laws needed by rational proof data. | 6 |
| math.nat.square-zero | nat/square-zero-implies-zero : a*a = 0 -> a = 0. | 1 |
| math.nat.strict-below-more | Small reusable nat lemmas for indexed-fold attainment (pure nat, off the trusted base): nat/add-successor-right : i + succ e = succ (i + e) (add recurses left, so this needs proof) nat/strict-below-self : m < succ m nat/strict-below-weaken : i < m -> i < succ m | 3 |
| math.nat.strict-below-split | nat/strict-below-successor-split : strict-below i (succ m) -> (strict-below i m) or (i = m). | 1 |