Reference
Logic
15 modules in src/rainbow/math/logic/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| math.logic.boolean-and | General soundness of the boolean AND used across the AHoF membership/monitor rows (interval containment, 2-D ODD boxes, polytope halfspaces, ...): and a b = if a then b else false (a Bool.rec over the first operand) Proved for ALL booleans a, b: and-implies-left : and a b = true -> a = true and-implies-right : and a b = true -> b = true and-sound : and a b = true -> (a = true) AND (b = true) The c | 3 |
| math.logic.clamp-range | Universal correctness of clamping (the PPO / trust-region clip of AHoF D52), built on the general nnrat min/max bounds: clamp r lo hi = min (max r lo) hi Proved for ALL r, lo, hi (not just worked instances): clamp-at-most-hi : clamp r lo hi <= hi lo-at-most-clamp : lo <= hi -> lo <= clamp r lo hi Together: whenever lo <= hi, the clamped value provably lies in the interval [lo, hi] for every input | 2 |
| math.logic.exhaustive-carrier-fintype | Constructively connect executable exhaustive carriers to extensional Fintype. | 2 |
| math.logic.finset | Extensional bundled finite sets as native Clojure proof data. | 14 |
| math.logic.fintype | Finite carrier data as an extensional complete native Finset. | 10 |
| math.logic.function-predicate | Checked native declarations for reusable higher-order function predicates. | 0 |
| math.logic.half-monotone | The general halving-monotonicity lemma for the convergence capstone: (1/2) * d <= d for every nonnegative rational d. | 1 |
| math.logic.infinite-injection | Classical, sort-polymorphic infinitude transport along injections. | 3 |
| math.logic.infinite-transport | Sort-polymorphic infinitude transport and a faithful native Int model. | 5 |
| math.logic.interval-membership-sound | Universal soundness of the two-clause interval/box membership test, composing the general boolean-AND soundness (rainbow.math.logic.boolean-and) with the decidable order: contains? | 1 |
| math.logic.maximum-expected-utility | AHoF D17: finite exact-rational maximum expected utility. | 7 |
| math.logic.scan-correctness | GENERAL (abstract-element) correctness theorems for the prefix-sum scan: for arbitrary list elements a, b, c the running totals are exactly the prefix sums, cumulative-sum [a] = [a] cumulative-sum [a, b] = [a, a + b] cumulative-sum [a, b, c] = [a, a + b, a + b + c]. | 3 |
| math.logic.scan-length | A GENERAL (for-all-inputs) correctness theorem about the prefix-sum scan: scanning a list preserves its length, length (cumulative-sum xs) = length xs for every list xs. | 2 |
| math.logic.strict-contraction-stabilization | Constructive bounded stabilization of strict contractions in a finite Nat sup metric. | 9 |
| math.logic.strict-contraction-uniqueness | Constructive uniqueness of support-relative fixed points for strict finite contractions. | 5 |