Reference
Non-negative rationals
140 modules in src/rainbow/math/rational/nnrat/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| math.rational.nnrat.add-cancel-zero | Additive cancellation to zero for nonnegative rationals: nnrat/add-cancel-to-zero : (a + g) ~ a -> g ~ 0 If adding g changes nothing, g was 0. | 1 |
| math.rational.nnrat.add-cancellation | Real-analysis roadmap step 3: additive cancellation for the nnrat order -- nnrat/at-most-add-right-cancel : (X + k) <= (Y + k) -> X <= Y the converse of add-monotonicity, and the piece signed order transitivity needs (it cancels the shared pos(b)+neg(b) term). | 2 |
| math.rational.nnrat.add-monotone | Universal (one-sided) monotonicity of nonnegative-rational addition under the rational order -- the additive companion to nnrat/multiply-monotone, and the keystone for convex-combination / weighted-average bounds: add-right-monotone-base : base-at-most a b -> base-at-most (a+c) (b+c) (all c a b) add-right-monotone : a <= b -> (a+c) <= (b+c) (all c a b) Base lemma is pure nat. | 5 |
| math.rational.nnrat.add-upper | The additive upper-bound law: a nonnegative rational is at most itself plus anything, `a <= a + b`. | 1 |
| math.rational.nnrat.add-zero-split | Nonnegativity forces zero: for nonnegative rationals, a sum equivalent to 0 forces each summand to 0. | 4 |
| math.rational.nnrat.additive-reassociation | Associativity and reusable summand reorder laws for native nonnegative rationals. | 3 |
| math.rational.nnrat.archimedean | The Archimedean reciprocal limit helper for nonnegative rationals. | 1 |
| math.rational.nnrat.commutative | Native commutativity of nonnegative-rational addition and multiplication, up to cross-multiplication equivalence. | 3 |
| math.rational.nnrat.complement-proper | Proper raw fraction for the exact complement of a positive subunit mass. | 2 |
| math.rational.nnrat.contraction-general | Generalized contraction convergence: ANY contraction rate gamma <= 1/2 drives the error to zero. | 1 |
| math.rational.nnrat.contraction-uniqueness | Banach fixed-point UNIQUENESS, the collapse half (the convergence half is nnrat-general-contraction). | 1 |
| math.rational.nnrat.convex | The convex-combination bound -- the capstone of the nnrat monotonicity + algebra foundation: convex-at-most-max : (w0 + w1) ~ 1 -> w0*v0 + w1*v1 <= max v0 v1 (all w0 w1 v0 v1) A weighted average with weights summing to one never exceeds the larger value -- the universal soundness behind every convex-combination / weighted-average step in the AHoF catalog (interpolation, exponential smoothing, mixi | 2 |
| math.rational.nnrat.convex-multi-point | Finite nonnegative-weighted combinations preserve global value bounds: sum_i (w i * m) <= sum_i (w i * v i) when forall i, m <= v i sum_i (w i * v i) <= sum_i (w i * Mx) when forall i, v i <= Mx These are the N-point convexity / averaging brackets without a normalization assumption on the weights. | 2 |
| math.rational.nnrat.convex-normalized | The normalized two-point convex bracket over nonnegative rationals. | 2 |
| math.rational.nnrat.convex-two-point | The unnormalized two-point convex-combination bracket over nonnegative rationals: (w0+w1)*min(v0,v1) <= w0*v0+w1*v1 <= (w0+w1)*max(v0,v1) The weights are arbitrary nonnegative rationals; they need not sum to one. | 2 |
| math.rational.nnrat.diagonal-spike | Canonical exact-rational diagonal spikes over duplicate-free finite carriers. | 10 |
| math.rational.nnrat.distance | A quotient-safe computational distance on exact nonnegative rationals. | 4 |
| math.rational.nnrat.distance-translation | Removing common nonnegative mass preserves exact rational distance. | 1 |
| math.rational.nnrat.distribute-right | Right-distributivity of nonnegative-rational multiplication over addition, carrying ONLY that law. | 1 |
| math.rational.nnrat.distributive | Right-distributivity of nonnegative-rational multiplication over addition, up to nnrat equivalence: multiply-distributes-add-right : (a + b) * m ~ a*m + b*m (all a b m) This is the last algebra brick for the convex-combination bound. | 2 |
| math.rational.nnrat.farkas-additive-cross | Brick 5c core of the general LP strong-duality Fourier-Motzkin encoding : the additive cross-elimination crux -- the necessary (certificate) direction, coefficient-1 case. | 1 |
| math.rational.nnrat.farkas-affine-cross | Brick 5c full of the general LP strong-duality Fourier-Motzkin encoding : the affine cross-elimination crux WITH COEFFICIENTS -- the coefficient wrapper around the additive core. | 1 |
| math.rational.nnrat.farkas-alternative | Constructive Farkas alternative for arbitrary finite nnrat elimination chains. | 12 |
| math.rational.nnrat.farkas-both-sides | Brick 5d-ii of the general LP strong-duality Fourier-Motzkin encoding : converting a both-sides row into a clean affine lower row, subtraction-free. | 2 |
| math.rational.nnrat.farkas-both-sides-reduce | Recursive-reduction sub-brick of brick 6 (single-row core): reduce a both-sides cross row to an affine row in the surviving variable. | 1 |
| math.rational.nnrat.farkas-bridge-list | Piece 1 of the n-variable capstone: the bridge-mapping -- map the structured bridge over a list of cross rows. | 1 |
| math.rational.nnrat.farkas-cross-bilist | Brick 6 (cross-product core) of the general LP strong-duality Fourier-Motzkin encoding: the cross-product over BOTH row lists -- a list of affine lower rows against a list of affine upper rows. | 1 |
| math.rational.nnrat.farkas-cross-bridge | Piece 1 core of the n-variable capstone: the structured bridge recognizing a cross condition as a both-sides row. | 1 |
| math.rational.nnrat.farkas-cross-list | Brick 5d-i of the general LP strong-duality Fourier-Motzkin encoding : the cross-product of one affine lower row against a LIST of affine upper rows. | 1 |
| math.rational.nnrat.farkas-cross-vectors | The unified representation, brick 3 core: one elimination cross at the coefficient-vector level. | 1 |
| math.rational.nnrat.farkas-cross-vectors-bilist | Brick 3 full round: cross a LIST of lower coefficient-vector constraints against a LIST of upper coefficient-vector constraints -- the whole round's reduced set. | 1 |
| math.rational.nnrat.farkas-cross-vectors-list | Brick 3 per-pair fold: cross one lower coefficient-vector constraint against a LIST of upper coefficient-vector constraints. | 1 |
| math.rational.nnrat.farkas-elim | A bounded first Fourier--Motzkin milestone over exact nonnegative rationals. | 3 |
| math.rational.nnrat.farkas-elim-affine-coupled | Brick 3 of the general LP strong-duality Fourier-Motzkin encoding : elimination of an nnrat variable v whose upper coupling carries an additive SURVIVOR-SUM term. | 3 |
| math.rational.nnrat.farkas-elim-affine-decidable | Brick 4b of the general LP strong-duality Fourier-Motzkin encoding : decidability of the one-variable affine-list elimination -- the Farkas-alternative half. | 2 |
| math.rational.nnrat.farkas-elim-affine-list | Brick 4 of the general LP strong-duality Fourier-Motzkin encoding : the one-primal-variable FM elimination step over a LIST of affine upper rows -- the first genuinely new formalization of the lane. | 3 |
| math.rational.nnrat.farkas-elim-affine-list-lower | Brick 5b of the general LP strong-duality Fourier-Motzkin encoding : the one-variable elimination step over a list of affine LOWER rows -- the mirror of brick 4 (nnrat_farkas_elim_affine_list.clj) for the other bound direction. | 3 |
| math.rational.nnrat.farkas-elim-chain | Arbitrary finite chains of constructive nnrat Fourier--Motzkin steps. | 6 |
| math.rational.nnrat.farkas-elim-coupled | Constructive elimination of an nnrat variable coupled to a survivor. | 3 |
| math.rational.nnrat.farkas-elim-list | List-sized one-variable Fourier--Motzkin elimination over nnrat bounds. | 9 |
| math.rational.nnrat.farkas-elim-scaled-coupled | Brick 1 of the general LP strong-duality Fourier-Motzkin encoding : elimination of an nnrat variable v that appears with a COEFFICIENT in its coupling to a survivor. | 3 |
| math.rational.nnrat.farkas-elim-scaled-coupled-lower | Brick 2 of the general LP strong-duality Fourier-Motzkin encoding : elimination of an nnrat variable v whose coupling to a survivor is a scaled LOWER bound. | 3 |
| math.rational.nnrat.farkas-elim-two-var | Constructive composition of list-sized elimination for two decoupled nnrat variables. | 3 |
| math.rational.nnrat.farkas-eliminate-all | The over-variable recursion: iterate one elimination round over the variable count. | 1 |
| math.rational.nnrat.farkas-eliminate-base | The over-variable recursion's base case: a fully-reduced constraint is a constant comparison. | 1 |
| math.rational.nnrat.farkas-eliminate-round | One full Fourier-Motzkin elimination round, composed : cross-product then reduction. | 1 |
| math.rational.nnrat.farkas-form-scale | The unified representation, brick 2 core: scaling a linear form scales its coefficient vector. | 1 |
| math.rational.nnrat.farkas-linear-form | The unified representation, brick 1: the coefficient-vector (linear-form) constraint type and the head-split extraction. | 2 |
| math.rational.nnrat.farkas-partition-covered | The vacuity FIX for the partition keystone: farkas-partition-list-necessary strengthened with a COVERING conjunct that ties the output partition to the input, killing the empty witness. | 1 |
| math.rational.nnrat.farkas-partition-list | Piece (ii) brick 1: the dependent partition of a reduced disjunction system into a lower-list and an upper-list. | 1 |
| math.rational.nnrat.farkas-partition-row | Piece (ii) brick 1 core: the per-row step of the dependent partition. | 1 |
| math.rational.nnrat.farkas-recursion-step | Piece (ii) recursion step: one full elimination round yields a feasible reduced lower/upper system. | 1 |
| math.rational.nnrat.farkas-recursion-step-covered | Covered recursion step (the vacuity fix, consumer migration): the affine elimination round built on the COVERING-strengthened partition keystone. | 1 |
| math.rational.nnrat.farkas-reduce-align | Piece (i) of the n-variable capstone: the data-representation alignment that lets the elimination round close on structured cross rows. | 2 |
| math.rational.nnrat.farkas-reduce-list | Recursive-reduction sub-brick of brick 6 (list form): map the single-row reduction over a list of both-sides cross rows. | 1 |
| math.rational.nnrat.farkas-reduced-list-satisfied | Farkas elimination REDUCTION CORRECTNESS (the SUFFICIENCY direction): nnrat/farkas-reduced-list-satisfied : forall rows w, farkas-reduced-conditions rows w -> farkas-both-sides-rows-satisfied rows w The existing forward theorem (reduce-list-necessary) proves satisfaction => reduced (reduced conditions are NECESSARY). | 1 |
| math.rational.nnrat.farkas-reduced-vector | The unified representation, brick 2 assembly : the cross condition expressed as a both-sides constraint over transformed coefficient vectors. | 1 |
| math.rational.nnrat.farkas-row-reconstruction | Reconstruct a source inequality from its reduced affine row and coefficient equation. | 2 |
| math.rational.nnrat.farkas-row-repackage | Brick 5a of the general LP strong-duality Fourier-Motzkin encoding : the row-repackaging crux, the one genuinely new proof obligation of the strong-duality payoff. | 1 |
| math.rational.nnrat.farkas-vector-adapter-bilist | The unified representation, partition bridge adapter (the bilist) : turn one whole elimination round's reduced conditions into the flat descriptor fold the bridge consumes. | 2 |
| math.rational.nnrat.farkas-vector-adapter-list | The unified representation, partition bridge adapter (per-upper list) : turn one round's per-lower reduced conditions into the flat descriptor fold the bridge consumes. | 1 |
| math.rational.nnrat.farkas-vector-both-sides | The unified representation, second-variable step: convert a reduced both-sides COEFFICIENT-VECTOR row into a lower/upper affine row in the next variable x2, subtraction-free. | 2 |
| math.rational.nnrat.farkas-vector-both-sides-reduce | The unified representation, per-row reduction: reduce a both-sides COEFFICIENT-VECTOR row to a lower/upper affine row in the next variable x2 -- as a disjunction, ready for the partition. | 1 |
| math.rational.nnrat.farkas-vector-partition-fold | The unified representation, partition bridge (the fold) : collect a LIST of reduced coefficient-vector rows into the affine partition's input. | 1 |
| math.rational.nnrat.farkas-vector-partition-pack | The unified representation, partition bridge (single row) : pack one reduced coefficient-vector row into a both-sides DATA row and discharge its reduced-conditions entry. | 1 |
| math.rational.nnrat.farkas-vector-round | The unified representation, one closed round: a feasible coefficient-vector system in k+1 variables yields a feasible affine system in k variables. | 1 |
| math.rational.nnrat.farkas-vector-round-covered | Covered coefficient-vector round (the vacuity fix, consumer migration): one Fourier-Motzkin round on the covering-strengthened partition keystone. | 1 |
| math.rational.nnrat.farkas-vector-step | The unified representation, the recursion step: one closed elimination step in the held next-variable representation, and its instantiation of the over-variable recursion skeleton. | 3 |
| math.rational.nnrat.farkas-vector-step-covered | Covered elimination step (the vacuity fix, consumer migration): one step in the held next-variable representation carrying the covering conjunct. | 1 |
| math.rational.nnrat.farkas-vector-unit-column | The unified representation, unit-column re-presentation : re-present a round's affine output rows as next-variable coefficient constraints, so the round's output feeds its own input and successive rounds chain. | 2 |
| math.rational.nnrat.farkas-vector-unit-repr-length | Length preservation of the unit-column re-presentation map (support for the covered step migration). | 1 |
| math.rational.nnrat.finite-min-positive | Positive lower bounds from finite exact-rational minima. | 4 |
| math.rational.nnrat.fubini | Fubini / double-sum swap for finite nnrat sums, up to nnrat equivalence (~): nnrat/map-sum-swap : sum_{i in is} sum_{j in js} F i j ~ sum_{j in js} sum_{i in is} F i j i.e. | 1 |
| math.rational.nnrat.general-contraction | Arbitrary-gamma contraction convergence. | 3 |
| math.rational.nnrat.general-harmonic | General harmonic null sequence, the bound that dominates any contraction rate gamma<1: nnrat/general-harmonic ap gp n := a / (a + n*g) with a = ap+1, g = gp+1 analysis/general-harmonic-null : rate-null (general-harmonic ap gp) (\k. | 1 |
| math.rational.nnrat.geometric-convergence | The geometric (contraction-rate) convergence payoff, fully self-contained: the sequence (1/2)^n converges to zero. | 4 |
| math.rational.nnrat.half-positive | nnrat/half-positive : 0 < half (as the reducible conjunction 0<=half AND not(0~half)). | 1 |
| math.rational.nnrat.harmonic-convergence | A CONCRETE convergence theorem: the harmonic sequence 1/(n+1) converges to zero, with an explicit modulus. | 3 |
| math.rational.nnrat.identities | Neutral and absorbing laws for native nonnegative rationals, up to cross-product equivalence. | 8 |
| math.rational.nnrat.inverse-gap-certificate | Sharp inverse-gap residual arithmetic directly in NNRAT. | 1 |
| math.rational.nnrat.lattice-monotone | Universal monotonicity of the exact-rational min and max under the rational order, composing the min/max bound + lattice-step theorems from rainbow.math.rational.nnrat.minmax: min-monotone : a<=a' -> b<=b' -> min a b <= min a' b' max-monotone : a<=a' -> b<=b' -> max a b <= max a' b' i.e. | 2 |
| math.rational.nnrat.list-sum | Finite sum of an nnrat-valued map over a list, and its monotonicity -- the n-ary generalization of nnrat/wsum2-monotone and the fold-level induction the scout flagged as the missing piece for dot-product / LP bounds: nnrat/map-sum A f xs = f x0 + f x1 + ... | 3 |
| math.rational.nnrat.lp-complementary | Complementary slackness for LP over nonnegative rationals -- the KKT optimality characterization, now a named machine-checked theorem. | 2 |
| math.rational.nnrat.lp-example | A concrete, fully worked LP with a machine-checked optimality certificate -- the tangible 'sellable' artifact: a real optimization instance whose proposed solution is PROVEN optimal by the kernel, with no trust in any solver. | 1 |
| math.rational.nnrat.lp-gap | LP duality-gap decomposition over nonnegative rationals -- the identity behind complementary slackness. | 1 |
| math.rational.nnrat.lp-multi-constraint-duality | Finite positive-constraint, one-variable LP duality over nnrat. | 5 |
| math.rational.nnrat.lp-optimality | LP optimality certificate over nonnegative rationals -- the sellable corollary of weak duality: a matching feasible primal/dual pair PROVES optimality. | 2 |
| math.rational.nnrat.lp-separable-multi-var | Zero total duality gap for a finite list of decoupled scalar nnrat LPs. | 1 |
| math.rational.nnrat.lp-separable-two-var | Strong duality for the sum of two decoupled scalar nnrat LPs. | 1 |
| math.rational.nnrat.lp-strong-duality | Concrete textbook strong duality for a verified Bool-indexed 2x2 LP. | 1 |
| math.rational.nnrat.lp-strong-duality-general | Constructive strong duality for a parametric scalar LP. | 8 |
| math.rational.nnrat.lp-two-var-strong-duality | Brick 5d-iii of the general LP strong-duality Fourier-Motzkin encoding : a two-variable strong-duality instance whose primal-optimality is proved BY THE FM ENGINE. | 2 |
| math.rational.nnrat.lp-weak-duality | LP weak duality over nonnegative rationals -- the frontier-OR capstone: primal max c.x s.t. | 1 |
| math.rational.nnrat.map-sum-additive | Additive congruences for nnrat/map-sum, up to nnrat equivalence (~) -- the Fubini prerequisites. | 2 |
| math.rational.nnrat.map-sum-append | Finite nnrat sums split over list concatenation, up to nnrat equivalence (~): nnrat/map-sum-append : map-sum f (append xs ys) ~ map-sum f xs + map-sum f ys The block/partition-decomposition law: the sum over a concatenated index list is the sum of the block sums. | 1 |
| math.rational.nnrat.map-sum-distance | Distance of finite NNRAT sums is bounded by the sum of distances. | 2 |
| math.rational.nnrat.map-sum-member | A listed nonnegative rational term is bounded by its finite sum. | 1 |
| math.rational.nnrat.map-sum-on | Compatibility entry point for the canonical member-restricted sum theorem. | 1 |
| math.rational.nnrat.map-sum-positive | Strict positivity of finite exact nonnegative-rational sums. | 1 |
| math.rational.nnrat.map-sum-respects | map-sum is a congruence for pointwise nnrat equivalence: nnrat/map-sum-respects-equivalence : (forall i, f i ~ g i) -> map-sum f is ~ map-sum g is Lets a per-term equivalence be rewritten underneath a finite sum -- the tool that applies map-sum-scale-right (and the per-term product reorder) inside the LP double sum. | 1 |
| math.rational.nnrat.map-sum-scale | Scalar pulls through a finite nnrat sum (scalar on the right), up to nnrat equivalence (~): nnrat/map-sum-scale-right : (map-sum f is) * c ~ map-sum (\i. | 1 |
| math.rational.nnrat.map-sum-zero | Every term of a vanishing finite nonnegative sum vanishes -- the sum-level form of nonnegativity-forces-zero, stated membership-free by positional split: nnrat/map-sum-zero-at-split : map-sum f (append ps (cons e qs)) ~ 0 -> f e ~ 0 i.e. | 1 |
| math.rational.nnrat.metric-separation | Exact separation for the computational NNRAT distance and finite radius. | 14 |
| math.rational.nnrat.minmax | General exact-rational min/max with UNIVERSAL (forall-quantified) order guarantees. | 6 |
| math.rational.nnrat.monus | Layer 2 of the signed->nnrat magnitude foundation: truncated subtraction on Nnrat. | 2 |
| math.rational.nnrat.multiply-commute | Standalone provider of nnrat/multiply-commutative (a*b ~ b*a), extracted so it can be chained WITHOUT nnrat_commutative's bundled nnrat/add-commutative, which alias-conflicts with nnrat_add_monotone's (different proof/sha). | 1 |
| math.rational.nnrat.multiply-difference-zero | General nnrat discriminant (both-ordered case): nnrat/multiply-difference-zero-ordered : N1<=P1 -> N2<=P2 -> (P1*P2 + N1*N2 ~ P1*N2 + N1*P2) -> (P1 ~ N1) or (P2 ~ N2). | 2 |
| math.rational.nnrat.multiply-monotone | Universal monotonicity of nonnegative-rational multiplication under the rational order -- the algebra gap flagged in rainbow-universal-foundation-layer that blocks convex-combination / weighted-average bounds: multiply-monotone-base : base-at-most a b -> base-at-most (c*a) (c*b) (all c a b) multiply-monotone : a <= b -> (c*a) <= (c*b) (all c a b) The base lemma is pure nat reasoning: with num/den | 2 |
| math.rational.nnrat.multiply-right-monotone | Right-factor monotonicity of nnrat multiplication under the rational order: nnrat/multiply-right-monotone : a <= b -> (a * c) <= (b * c) The mirror of rainbow.math.rational.nnrat.multiply-monotone (left factor). | 2 |
| math.rational.nnrat.multiply-zero-split | nnrat/multiply-zero-split : m1*m2 ~ 0 -> (m1 ~ 0) or (m2 ~ 0). | 1 |
| math.rational.nnrat.null-scaling | Scaling a null sequence by a bounded constant preserves convergence to zero: analysis/rate-null-scaled : c <= 1 -> rate-null s M -> rate-null (\n. | 1 |
| math.rational.nnrat.null-sequence | Real-analysis toward the OR payoff: null (converging-to-zero) sequences of nonnegative rationals, and the COMPARISON TEST -- a sequence dominated by a null sequence is null. | 2 |
| math.rational.nnrat.order-difference | Nonnegative-rational order is difference-existence, and the two-point rearrangement inequality that follows from it. | 2 |
| math.rational.nnrat.order-equivalence | Real-analysis roadmap step 2: the nnrat closure<->base order equivalence. | 2 |
| math.rational.nnrat.order-nontrivial | Constructive impossibility of 1 <= 0 and of k+1 <= k+0 in nnrat order. | 2 |
| math.rational.nnrat.order-scale | Positive scaling and coefficient normalization for the nnrat order. | 5 |
| math.rational.nnrat.order-total | Totality of the nnrat order: for all a b, a <= b OR b <= a. | 1 |
| math.rational.nnrat.ordered-distance | Exact reconstruction from ordered nonnegative-rational distance. | 2 |
| math.rational.nnrat.positive | Constructive strict positivity for exact nonnegative rationals. | 10 |
| math.rational.nnrat.positive-monotone | B6c of the limit-reciprocal arc: positivity of an nnrat is preserved upward under <=. | 2 |
| math.rational.nnrat.positive-succ-form | A positive nnrat in make(succ p, q) form, so the reciprocal machinery (divide-self-positive / reciprocal-scale-cancel, which are stated for make(succ p, q)) applies to it. | 2 |
| math.rational.nnrat.power | Exact powers of a nonnegative rational. | 0 |
| math.rational.nnrat.product-reassociation | Associativity and factor reassociation for native nonnegative rationals. | 3 |
| math.rational.nnrat.quadratic-zero | Zero reflection and the equality case of the nnrat square inequality. | 3 |
| math.rational.nnrat.radius-cancel | The reciprocal radius-cancellation for a general positive nnrat, the linchpin of the limit-product modulus. | 1 |
| math.rational.nnrat.ring | A verified nonnegative-rational semiring normalization tactic, up to `nnrat/equivalent`. | 0 |
| math.rational.nnrat.shared-residual-mass | Canonical common/residual decomposition, computed without choice. | 5 |
| math.rational.nnrat.square-difference-zero | The nnrat AM-GM discriminant, ordered case: nnrat/square-difference-zero-ordered : N<=P -> (P*P + N*N ~ P*N + N*P) -> P ~ N. | 2 |
| math.rational.nnrat.square-positive | nnrat/square-positive : positive k -> positive (k*k). | 1 |
| math.rational.nnrat.square-zero | nnrat/square-zero : m*m ~ 0 -> m ~ 0. | 1 |
| math.rational.nnrat.strict-order | Strict order on nonnegative rationals -- the nnrat mirror of signed_strict_order, needed for the no-zero-divisors pair theorem (which case-splits on the nnrat order of a signed value's positive/negative components). | 8 |
| math.rational.nnrat.unit-fraction | Explicit positive unit fractions and their proper complements. | 4 |
| math.rational.nnrat.value-iteration | The self-contained value-iteration convergence theorem: a contraction recurrence drives the error to zero. | 5 |
| math.rational.nnrat.weighted-dot | Weighted sum (dot product) of nonnegative-rational coordinate functions over an index list, and its monotonicity in the value coordinates: nnrat/weighted-sum A c x is = sum_i (c i) * (x i) over is : List A nnrat/weighted-sum-monotone : (forall i, x i <= x' i) -> weighted-sum c x is <= weighted-sum c x' is This is the LP objective-bound engine: with nonnegative weights c, dominating the values coor | 1 |
| math.rational.nnrat.weighted-map-sum-distance | Weighted distance lift using the canonical scalar scaling theorem. | 0 |
| math.rational.nnrat.weighted-sum | Universal monotonicity of a two-term nonnegative-rational weighted sum in its values -- the first composite guarantee assembled from the monotonicity foundation (nnrat/multiply-monotone + nnrat/add-monotone): wsum2 w0 w1 v0 v1 = w0*v0 + w1*v1 wsum2-monotone : v0 <= v0' -> v1 <= v1' -> wsum2 w0 w1 v0 v1 <= wsum2 w0 w1 v0' v1' (all w0 w1 v..) i.e. | 1 |
| math.rational.nnrat.weighted-sum-bound | Finite-list lift of weighted-term monotonicity. | 0 |
| math.rational.nnrat.weighted-sum-scaled-bound | Compose the finite weighted-sum bound with right-scaling of a sum. | 0 |
| math.rational.nnrat.weighted-sum-scaling | Publicly named finite-sum scaling bridge for contraction proofs. | 0 |
| math.rational.nnrat.weighted-term-bound | Scalar weighted-term monotonicity for the finite mixture proof. | 1 |