Reference
Foundations
8 modules in src/rainbow/math/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| math.checks | General lemmas: checks. | 12 |
| math.constructive-unique-fixed-point | Constructive existence and support-relative uniqueness for strict Nat contractions. | 3 |
| math.monte-carlo-estimation | Direct Monte Carlo estimation of a failure probability. | 3 |
| math.nonnegative-rational | Nonnegative rationals as proof data: numerator plus denominator predecessor. | 6 |
| math.or-foundation | Small reusable proof-data laws shared by OR representations. | 1 |
| math.prelude | 0 | |
| math.real-analysis-foundation | FIRST brick of the real-analysis layer -- the gating foundation for frontier OR (convergence rates, GP regret, MDP contraction, LP duality all live over the reals). | 2 |
| math.temporal-difference | Bounded temporal-difference (Q-learning) updates over signed rationals. | 3 |