Reference
Finite types, distributions and Markov chains
122 modules in src/rainbow/math/finite/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| math.finite.async-value-iteration | Asynchronous (Gauss-Seidel) finite Bellman value iteration. | 6 |
| math.finite.bellman | Exact scaled finite transition rows and fixed-policy Bellman numerators. | 7 |
| math.finite.bellman-backup-contraction | Discount-scaled contraction of finite NNRAT Bellman backups and T*. | 2 |
| math.finite.bellman-fixed-point-uniqueness | Constructive uniqueness of exact finite NNRAT Bellman optimality fixed points. | 3 |
| math.finite.bellman-greedy-policy-optimal | Fully concrete greedy-policy extraction for exact finite NNRAT Bellman models. | 3 |
| math.finite.bellman-iterate-monotone | A post-fixed nnrat value function lies below every finite iterate of the Bellman optimality operator. | 5 |
| math.finite.bellman-monotone | Monotonicity of finite nnrat expectations, Bellman action backups, and the Bellman optimality operator. | 4 |
| math.finite.bellman-optimal-contraction | Finite-argmax nonexpansiveness for the NNRAT Bellman optimality layer. | 4 |
| math.finite.bellman-optimality | Bellman optimality, operator level: the optimal (greedy / max-over-actions) Bellman backup dominates every fixed-policy backup. | 2 |
| math.finite.bellman-policy-residual-certificate | Residual certificates and uniqueness for exact finite fixed-policy Bellman operators. | 8 |
| math.finite.bellman-residual-certificate | A posteriori certificates for exact finite NNRAT Bellman solvers. | 4 |
| math.finite.bellman-signed-action-backup | Concrete signed Bellman action backups and their additive contraction. | 3 |
| math.finite.bellman-signed-approximate-optimality | Constructive approximate fixed points of signed Bellman optimality. | 2 |
| math.finite.bellman-signed-approximate-optimality-generic | Approximate fixed points for a certified finite signed Bellman operator. | 3 |
| math.finite.bellman-signed-fixed-point-uniqueness | Uniqueness of signed Bellman optimality fixed points. | 1 |
| math.finite.bellman-signed-greedy-policy | Greedy policy extraction from a signed Bellman fixed point. | 3 |
| math.finite.bellman-signed-operator-fixed-point-convergence | Fixed-point convergence of the low-arity signed operator iterator. | 4 |
| math.finite.bellman-signed-optimal-contraction | Signed finite Bellman optimality inherits action-backup contraction. | 1 |
| math.finite.bellman-signed-optimality | Generic finite Bellman optimality over exact signed-rational action scores. | 6 |
| math.finite.bellman-signed-policy | Signed-reward fixed-policy Bellman certificates in finite matrix form. | 9 |
| math.finite.bellman-signed-policy-approximate-fixed-point | Constructive approximate fixed points for finite signed policy evaluation. | 6 |
| math.finite.bellman-signed-policy-dominance | Dominance of admissible signed policy values by Bellman optimality. | 10 |
| math.finite.bellman-signed-policy-optimal | Concrete signed greedy-policy optimality for finite Bellman models. | 8 |
| math.finite.bellman-signed-policy-sensitivity | Robustness of signed fixed-policy Bellman evaluations under model drift. | 1 |
| math.finite.bellman-signed-residual-certificate | A posteriori residual certificates for signed Bellman optimality. | 4 |
| math.finite.bellman-signed-transition-approximate-optimality | Constructive approximate optimality for normalized finite signed MDPs. | 4 |
| math.finite.bellman-signed-transition-bridge | Embed ordinary nonnegative transition kernels into signed Bellman proofs. | 5 |
| math.finite.bellman-signed-transition-operator | Named concrete signed Bellman operator over ordinary nnrat transitions. | 6 |
| math.finite.bellman-signed-value-iteration | Finite-horizon signed Bellman value-iteration envelopes. | 5 |
| math.finite.bellman-signed-value-iteration-converges | Rate-null convergence certificate for signed Bellman value iteration. | 3 |
| math.finite.bellman-signed-value-iteration-general-converges | General strict-rate convergence for signed Bellman value iteration. | 6 |
| math.finite.bellman-stationary-policy-optimal | A concrete optimal-policy theorem for exact finite NNRAT Bellman models. | 1 |
| math.finite.bellman-value-iteration-converges | Uniform additive convergence bounds for finite Bellman value iteration. | 15 |
| math.finite.bellman-value-optimality | Normalized finite NNRAT expectation bounds and Bellman contractions. | 7 |
| math.finite.bellman-value-optimality-theorem | Abstract, reduction-safe capstones for finite Bellman value iteration. | 4 |
| math.finite.expectation | Executable finite natural mass and expectation numerators. | 4 |
| math.finite.greedy-optimal | Greedy policy extraction from a finite nnrat Bellman fixed point. | 3 |
| math.finite.index | Axiom-free bounded indices as a structural finite family. | 13 |
| math.finite.index-hastings | The canonical Hastings kernel instantiated on structural finite indices. | 3 |
| math.finite.index-hastings-coefficient | Explicit proper Dobrushin factors for canonical Hastings on Index(n+1). | 2 |
| math.finite.index-hastings-ergodic | The finite ergodic theorem, instantiated for canonical Hastings kernels. | 2 |
| math.finite.markov-aperiodicity | Aperiodicity from exact finite-state return horizons. | 2 |
| math.finite.markov-cesaro | Finite Cesaro occupation sums and averages for exact NNRAT Markov dynamics. | 8 |
| math.finite.markov-column-exact-contraction | Exact column-minimum coefficient and its positive-total properness. | 7 |
| math.finite.markov-column-minorization | Construct a shared lower mass by taking a finite minimum in each column. | 4 |
| math.finite.markov-contraction-uniqueness | Stationary-distribution uniqueness, conditional on one named inequality. | 1 |
| math.finite.markov-coupling-coefficient | Charge off-diagonal residual coupling costs to the Dobrushin coefficient. | 3 |
| math.finite.markov-coupling-distance | Off-diagonal kernel-row distance bound from a coupling's two marginals. | 3 |
| math.finite.markov-dobrushin | Maximum of a supplied NNRAT distance list, for a finite Dobrushin coefficient. | 4 |
| math.finite.markov-dobrushin-contraction | Inhabitant of the frozen finite Dobrushin contraction predicate. | 2 |
| math.finite.markov-dobrushin-kernel | Dobrushin coefficient constructed from every pair of enumerated kernel rows. | 4 |
| math.finite.markov-dobrushin-statement | Formal proposition for the finite Dobrushin contraction estimate. | 0 |
| math.finite.markov-ergodic-hypotheses | The exact finite-chain hypotheses needed by a future ergodic theorem. | 3 |
| math.finite.markov-ergodic-uniqueness | Uniqueness of stationary distributions under a certified Dobrushin bound. | 1 |
| math.finite.markov-expectation-invariance | Exact observable invariance under stationary finite Markov dynamics. | 3 |
| math.finite.markov-expectation-tower | The exact finite Markov expectation tower law over NNRAT. | 2 |
| math.finite.markov-full-support | An executable full-support decision, and what its verdict is worth. | 5 |
| math.finite.markov-full-support-irreducible | Executable full support certifies irreducibility of finite Index kernels. | 3 |
| math.finite.markov-geometric-convergence | Iterates converge to the stationary distribution at geometric rate. | 1 |
| math.finite.markov-geometric-decay | Geometric decay of total variation along kernel iterates. | 1 |
| math.finite.markov-hastings-diagonal | The canonical diagonal rejection placement, from a Boolean equality decider. | 4 |
| math.finite.markov-hastings-flow | General, division-free Hastings accepted-flow certificates. | 27 |
| math.finite.markov-hastings-positive | Strict-positivity certificates for division-free Hastings transitions. | 5 |
| math.finite.markov-iteration | Certified finite-horizon iteration of an exact NNRAT Markov kernel. | 6 |
| math.finite.markov-iteration-semigroup | Semigroup law for finite exact-rational Markov iteration. | 1 |
| math.finite.markov-kernel-algebra | Congruence, associativity, and observable action for exact finite kernels. | 5 |
| math.finite.markov-kernel-composition | Composition laws for exact finite NNRAT Markov kernels. | 5 |
| math.finite.markov-kernel-composition-positive | Positive witnesses for finite exact-rational kernel composition. | 2 |
| math.finite.markov-kernel-minimum | A certified global minimum entry of a finite exact-rational kernel. | 5 |
| math.finite.markov-metropolis-hastings | A fully checked finite Metropolis--Hastings independence sampler. | 8 |
| math.finite.markov-minorization | Finite shared lower-mass certificates for Dobrushin bounds. | 3 |
| math.finite.markov-minorization-complement | Exact complementary-mass bounds, without a raw-denominator approximation. | 3 |
| math.finite.markov-mixture-statement | Formal target for the finite residual-mixture inequality used by Dobrushin. | 0 |
| math.finite.markov-overlap | Shared-mass certificates for finite Dobrushin bounds. | 6 |
| math.finite.markov-point-mass | Canonical point masses for finite exact-rational Markov kernels. | 7 |
| math.finite.markov-positive-coefficient | Explicit Dobrushin factors from a positive finite kernel minimum. | 2 |
| math.finite.markov-positive-step | Positive support propagation through a finite exact-rational kernel. | 3 |
| math.finite.markov-reachability | Finite-step reachability and irreducibility for exact finite Markov kernels. | 4 |
| math.finite.markov-reachability-witness | Existential finite-horizon witnesses for exact-rational Markov support. | 2 |
| math.finite.markov-residual-coupling | Residual mass balance and constructive product-coupling marginals. | 5 |
| math.finite.markov-residual-expansion | Canonical common mass cancels after a kernel step. | 5 |
| math.finite.markov-residual-mixture-bound | Markov-facing interface for the finite residual mixture inequality. | 0 |
| math.finite.markov-return-time | Fixed-horizon return evidence for exact finite Markov kernels. | 2 |
| math.finite.markov-stationarity | Exact finite NNRAT Markov kernels, detailed balance, and stationarity. | 5 |
| math.finite.markov-stationary-iterate | A stationary distribution is fixed by every kernel iterate. | 1 |
| math.finite.markov-total-variation | Total-variation distance between finite exact-rational distributions, and the separation half of the coming ergodic theorem. | 6 |
| math.finite.markov-total-variation-bound | Normalized finite total variation and its stochastic-row unit bound. | 5 |
| math.finite.markov-total-variation-translation | Common finite mass cancels from L1 and normalized total variation. | 2 |
| math.finite.matrix | Finite signed-rational matrices and their native action on vectors. | 3 |
| math.finite.metric | Constructive maximum folds and finite sup-distance over exact finite data. | 11 |
| math.finite.metric-separation | Constructive zero and positivity separation for finite natural sup-distance. | 6 |
| math.finite.nnrat-sup-distance | A native finite supremum metric for NNRAT-valued functions. | 6 |
| math.finite.nnrat-sup-radius | A Bellman-compatible NNRAT supremum radius over exact finite carriers. | 6 |
| math.finite.policy-evaluation | AHoF D20: bounded finite-policy evaluation over exact rational data. | 6 |
| math.finite.policy-improvement | Policy-iteration monotonic improvement (Q-score level): the greedy-improved policy's action-score dominates the current policy's at every state. | 1 |
| math.finite.policy-iteration | Finite exact-rational policy improvement and one composed iteration step. | 7 |
| math.finite.policy-iteration-optimal | Stationary finite-policy improvement implies the optimal Bellman equation. | 2 |
| math.finite.policy-value-dominance | Abstract, reduction-safe policy-improvement value dominance for finite nnrat MDPs. | 3 |
| math.finite.powerset | Finite powersets, infinite suprema, and subtype projection injectivity. | 4 |
| math.finite.rational-argmax | Executable finite argmax with exact rational dominance certificates. | 15 |
| math.finite.rational-argmin | Executable finite argmin with exact rational minimality certificates. | 8 |
| math.finite.rational-expectation | Finite nonnegative-rational folds and expectations with congruence proofs. | 2 |
| math.finite.set | Constructive finite-set theorems over native List-cover proof data. | 27 |
| math.finite.set-boundary | Classical boundary facts for native finite and infinite sets. | 6 |
| math.finite.set-classical | Classical finite-set transport, kept separate from the axiom-free layer. | 11 |
| math.finite.set-fiber | Constructive finite fibers inside finite source sets. | 4 |
| math.finite.set-fiber-decomposition | A finite source is the union of its fibers over its finite image. | 4 |
| math.finite.set-image2-infinite | Infinitude transport through binary images and Cartesian products. | 4 |
| math.finite.set-indexed-union | Constructive finite unions over finite index sets. | 8 |
| math.finite.set-inverse-transport | Constructive finiteness and infinitude transport across explicit set inverses. | 5 |
| math.finite.set-lattice | Finite-set closure facts for complements, intersections, and suprema. | 4 |
| math.finite.set-union | Reusable finite/infinite union facts as native proof data. | 5 |
| math.finite.signed-approximate-fixed-point-sup | Finite-sup certificates from pointwise signed approximate fixed points. | 3 |
| math.finite.signed-argmax | Executable finite argmax over exact signed-rational scores. | 8 |
| math.finite.signed-argmax-nonexpansive | Additive nonexpansiveness of runtime-length finite signed-rational argmax. | 2 |
| math.finite.signed-expectation | Normalized finite expectation for exact signed-rational outcomes. | 3 |
| math.finite.signed-sup-distance | A native finite supremum metric for signed-valued functions. | 5 |
| math.finite.signed-sup-separation | Exact separation for finite signed-valued function sup distance. | 3 |
| math.finite.subtype | Finite propositions and finite-subtype bridges as checked proof data. | 5 |
| math.finite.type | Native finite and infinite carrier propositions as finite List covers. | 5 |
| math.finite.value-iteration | Finite Bellman optimality and bounded value iteration over exact rationals. | 7 |
| math.finite.vector | Finite vectors over signed rationals: lists of signed-rational components with elementwise addition, negation, subtraction, and scalar scaling. | 5 |