Reference
Finite sums
37 modules in src/rainbow/math/sums/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| math.sums.admissions-block | A blocking indicator vanishes exactly when the student does not improve, or the college has neither vacancy nor rank improvement. | 2 |
| math.sums.binary-capacity | For binary entries, x+y<=1 means selecting x excludes y. | 3 |
| math.sums.binary-conflicts | Reusable bridges from binary entries and nonpositive nonnegative sums to exclusions. | 3 |
| math.sums.binary-mutuality | Mutual selected-edge implications identify binary entries. | 1 |
| math.sums.boolean-predicate | The converse of the existing zero/one polynomial lemma, for predicate adapters. | 1 |
| math.sums.bpath-cut | Cut/exit proof support for bottleneck paths. | 4 |
| math.sums.bpath-walk | Finite one-hot walks crossing a binary cut. | 8 |
| math.sums.budgeted-protection | Weak duality for a budgeted box: 0<=w<=1, sum w<=Gamma and d_j<=z+p_j, z,p>=0 imply sum w_j*d_j<=Gamma*z+sum p_j. | 2 |
| math.sums.earliest-schedule | The earliest-start recurrence preserves feasibility whenever any window schedule exists. | 6 |
| math.sums.equality-lp-bound | Weak duality for equality rows and unrestricted dual prices. | 1 |
| math.sums.flow-cut | General lemmas: flow cut. | 9 |
| math.sums.indicator-zero | A zero sum of strict-violation indicators means every weak inequality holds. | 4 |
| math.sums.lp-bounds | Finite covering duality and certificate-gap arithmetic, reusing the existing list-backed LP theorem. | 4 |
| math.sums.lp-mixed-bound | A free-price equality block, nonnegative-price upper rows and unit upper bounds. | 4 |
| math.sums.lp-two-blocks | Weak duality with two separate constraint blocks, by two applications of the existing LP theorem. | 1 |
| math.sums.nonblocking | An encoded maximum is nonnegative exactly when at least one preference gap is. | 4 |
| math.sums.nonneg-zero | Nonnegative terms that sum to zero are each zero, over signed/expr-sum-value: if 0 <= F i for every i < k and sum F k ~ 0 then F i ~ 0 for every i < k. | 3 |
| math.sums.of-nat | The bridge between a natural-number count written as the signed literal of-nat n = n/1 (the form the checkers use, e.g. | 3 |
| math.sums.one-hot-factor | Reusable selection factorization for arbitrary signed values. | 2 |
| math.sums.one-hot-index | Every selected index reads every one-hot weighted sum; every distinct index is zero. | 3 |
| math.sums.one-hot-pair | Two independent one-hot rows select exactly the corresponding matrix entry. | 2 |
| math.sums.one-hot-value | Pointwise values of a selected index, their weighted equality, and explicit attainment. | 3 |
| math.sums.pareto-mask | The Pareto penalty mask is equivalent to absence of strict gain under componentwise dominance. | 4 |
| math.sums.period-usage | Multiplying two Boolean indicators by a weight equals filtering that weight by both tests. | 1 |
| math.sums.permutation-invariant | Nonlinear two-coordinate sums are invariant under a binary permutation matrix. | 3 |
| math.sums.predicate-bridges | Reusable bridges from checker indicators and squared norms to mathematical predicates. | 3 |
| math.sums.selected-minimum | A one-hot selected minimum among non-excluded entries. | 2 |
| math.sums.single-support | Single supported terms and tight finite unit-capacity sums. | 6 |
| math.sums.strict-indicator | A strict comparison indicator is one exactly when the reverse weak inequality is false. | 3 |
| math.sums.triangular | Triangular decomposition for the existing finite sums; prefix completion costs. | 4 |
| math.sums.two-terms | One term, and two DISTINCT terms, are bounded by a nonnegative expr-sum-value. | 2 |
| math.sums.value-algebra | Finite-sum algebra for the existing signed/expr-sum-value. | 11 |
| math.sums.value-append | Split the existing expr-sum-value at any Nat offset a: sum F (b+a) ~ sum F a + sum (fn i. | 1 |
| math.sums.wspt-order | WSPT order prerequisites. | 5 |
| math.sums.wspt-pair-bound | Pairwise lower bound for a prefix completion objective, exact for sorted pairs. | 4 |
| math.sums.wspt-permutation | WSPT optimality over all permutation matrices, with positive processing times. | 4 |
| math.sums.zero-violations | Zero positive-part penalties mean no violated inequality; a minimum encodes disjunction. | 8 |