Reference
Algorithm guarantees
85 modules in src/rainbow/algorithms/proofs/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| algorithms.proofs.adadelta | AHoF O23 Adadelta: the learning-rate-free update scale. | 3 |
| algorithms.proofs.adam | AHoF O24 Adam: the first-moment (momentum) estimate and the preconditioned step direction. | 3 |
| algorithms.proofs.adaptive-gradient | AHoF O21 AdaGrad: the adaptive per-parameter learning rate. | 4 |
| algorithms.proofs.admm | AHoF O51 ADMM (Alternating Direction Method of Multipliers): the scaled-form dual variable update over vector-valued state. | 3 |
| algorithms.proofs.argmax-index | Argmax over a list of nonnegative rationals, returning the INDEX of the maximum element (the first index attaining it): argmax-index [x0, x1, ...] = the i minimizing (-x_i), ties to the earliest. | 3 |
| algorithms.proofs.augmented-lagrangian | AHoF O49 Augmented Lagrangian: the dual multiplier update in the outer loop. | 3 |
| algorithms.proofs.bayesian-learning | Bayesian parameter learning over exact rationals. | 2 |
| algorithms.proofs.bellman-contraction | Finite fixed-policy Bellman contraction over exact natural numerators. | 5 |
| algorithms.proofs.bellman-scaled-fixed-point-uniqueness | Constructive uniqueness of scaled fixed points for finite Bellman numerators. | 10 |
| algorithms.proofs.bisection | Bisection bracket search over exact nonnegative rationals. | 3 |
| algorithms.proofs.box-projection | AHoF box projection (the projection step of Projected Gradient Descent and box-constrained optimization): after an unconstrained gradient step lands at x, the iterate is projected back onto the feasible box [lo, hi] by clamping, clamp lo hi x = max(lo, min(x, hi)) using the decidable rational order. | 5 |
| algorithms.proofs.branch-and-bound | AHoF D34 / O-family Branch and Bound: the bounding test that turns exhaustive enumeration into a pruned search. | 3 |
| algorithms.proofs.composite-metric | Composite evaluation metrics over exact rationals. | 1 |
| algorithms.proofs.conjugate-gradient | Conjugate gradient descent over signed rationals with pair-valued state. | 3 |
| algorithms.proofs.coordinate-search | Cyclic coordinate search over signed-rational pair state. | 4 |
| algorithms.proofs.counterfactual | AHoF V57 Counterfactual Explanation: the proximity term of the counterfactual search objective. | 2 |
| algorithms.proofs.counterfactual-distance-laws | Native algebraic laws for exact counterfactual squared distance. | 3 |
| algorithms.proofs.counterfactual-distance-separation | Native separation laws for the existing counterfactual squared distance. | 4 |
| algorithms.proofs.counterfactual-objective-laws | Native guarantees for the exact counterfactual optimization objective. | 4 |
| algorithms.proofs.cross-validation | K-fold cross-validation mean over exact rationals. | 2 |
| algorithms.proofs.cuckoo-search | AHoF O47 Cuckoo Search: the Levy-flight step over vector-valued state. | 3 |
| algorithms.proofs.decision-guarantee-audit | Finite exact-rational decision-bound auditing as native proof data. | 11 |
| algorithms.proofs.decision-network | Decision network evaluation over exact rationals. | 1 |
| algorithms.proofs.differential-evolution | AHoF O44 Differential Evolution: the differential mutation over vector-valued population members. | 4 |
| algorithms.proofs.dual-ascent | AHoF O52 Dual Ascent: the dual-variable ascent step over vector-valued multipliers. | 3 |
| algorithms.proofs.edit-distance | AHoF edit distance / Levenshtein alignment DP cell. | 4 |
| algorithms.proofs.eligibility-traces | Eligibility traces (TD(lambda)) over exact rationals. | 2 |
| algorithms.proofs.exact-inference | Exact Bayesian inference by enumeration over a finite hidden variable. | 4 |
| algorithms.proofs.factorial | AHoF factorial n! | 4 |
| algorithms.proofs.failure-probability-monitor | Runtime failure-probability monitoring over exact rationals (AHoF V64). | 2 |
| algorithms.proofs.feature-importance | AHoF V54 Permutation Feature Importance: the drop in model score when a feature's values are permuted, measuring how much the model relies on it: importance(feature) = baseline-score - permuted-score a signed subtraction (the drop is usually positive but can be negative for a harmful feature). | 3 |
| algorithms.proofs.fibonacci | AHoF Fibonacci numbers -- the linear recurrence behind Fibonacci search (the derivative-free line-search that places probes at Fibonacci ratios) and a canonical dynamic-programming example. | 4 |
| algorithms.proofs.firefly | AHoF O46 Firefly Algorithm: the attraction move over vector-valued state. | 3 |
| algorithms.proofs.floyd-warshall | AHoF Floyd-Warshall all-pairs shortest paths -- the dynamic-programming relaxation through an intermediate node. | 3 |
| algorithms.proofs.full-factorial | AHoF O58 Full Factorial Sampling: the design size is the product of the per-dimension level counts. | 4 |
| algorithms.proofs.general-descent | The general descent skeleton over signed rationals: the parent of the whole descent family. | 3 |
| algorithms.proofs.golden-section-search | Golden Section Search interval reduction over exact rationals (AHoF O9). | 2 |
| algorithms.proofs.gradient-ascent | Bounded fixed-rate gradient ascent over exact nonnegative rationals. | 4 |
| algorithms.proofs.gradient-descent | Bounded fixed-rate gradient descent over signed rationals. | 3 |
| algorithms.proofs.histogram-bin | AHoF histogram / kernel-density bin count: the number of sample values that fall inside a half-open-style bin [lo, hi], count-in-range lo hi xs = |{ x in xs : lo <= x and x <= hi }|, the primitive behind histograms and (boxcar-kernel) density estimation. | 4 |
| algorithms.proofs.hooke-jeeves | AHoF O34 Hooke-Jeeves pattern search: the exploratory probe and the pattern (acceleration) move over vector-valued state. | 5 |
| algorithms.proofs.hypergradient | AHoF O25 Hypergradient Descent: the meta-optimizer that tunes its own learning rate by the gradient of the loss with respect to the learning rate. | 3 |
| algorithms.proofs.importance-sampling | Likelihood-weighted (importance) sampling estimates over exact rationals. | 2 |
| algorithms.proofs.inner-product | The vector dot product (inner product) over signed-rational vectors: dot [a1..an] [b1..bn] = sum_i a_i * b_i This is a zip of the two component lists with signed multiplication, summed with signed addition -- a nested `data/List.rec` that reduces the two vectors to a single signed scalar (the shape of `vector/add`, but accumulating a sum of products rather than a vector). | 3 |
| algorithms.proofs.interior-point | AHoF O50 Interior Point / Barrier Method: the transform that keeps iterates strictly feasible by adding a barrier term that grows as a constraint slack approaches zero: barrier-objective = objective + mu * (1 / slack) where `slack` is the (positive) distance to a constraint boundary and `mu` is the barrier parameter, shrunk toward zero across outer iterations. | 3 |
| algorithms.proofs.interval-arithmetic | AHoF V40 Interval Arithmetic: the sound enclosure of a signed-rational value by a lower/upper bound pair, with the additive interval operation that underlies the reachability propagators (V40-V47). | 5 |
| algorithms.proofs.interval-membership | Interval membership over exact rationals (AHoF V40, decision layer). | 2 |
| algorithms.proofs.latin-hypercube | AHoF O59 Latin Hypercube Sampling: a space-filling design that draws exactly n sample points across any number k of dimensions, in contrast to the full factorial design (O58) whose size grows as the product of per-dimension level counts. | 4 |
| algorithms.proofs.levenberg-marquardt | Levenberg-Marquardt as the general descent skeleton with a damped Hessian-inverse step size. | 1 |
| algorithms.proofs.list-maximum | Maximum of a list of nonnegative rationals, as a native fold: list-maximum [x0, x1, ...] = max(x0, max(x1, ... | 4 |
| algorithms.proofs.list-product | Product of a list of nonnegative rationals, as a native fold: list-product [x0, x1, ...] = x0 * x1 * ... | 3 |
| algorithms.proofs.local-search | Bounded local (hill-climbing) search over a finite candidate set with exact rational objectives. | 5 |
| algorithms.proofs.maximum-likelihood | Maximum likelihood estimation over exact rationals. | 2 |
| algorithms.proofs.metropolis | AHoF V22 Metropolis-Hastings acceptance (also the acceptance rule of Simulated Annealing): a proposed state is scored by an energy (cost), and the Metropolis rule always accepts a downhill proposal, while an uphill proposal is accepted only with probability exp(-(E' - E)/T). | 3 |
| algorithms.proofs.minimax | AHoF adversarial decision-making -- the minimax value of a two-ply zero-sum game. | 3 |
| algorithms.proofs.momentum | Polyak momentum descent over signed rationals with pair-valued state. | 4 |
| algorithms.proofs.nearest-neighbor | Nearest-neighbor value function approximation over exact rationals. | 1 |
| algorithms.proofs.nelder-mead | AHoF O36 Nelder-Mead Simplex: the reflection move, the workhorse simplex transform. | 2 |
| algorithms.proofs.nesterov | Nesterov accelerated momentum over signed rationals with pair-valued state. | 4 |
| algorithms.proofs.net-flow | AHoF net flow / net present value: the signed balance of inflows against outflows, net inflow outflow = inflow - outflow, the exact-rational primitive behind net-reward MDPs, cash-flow / NPV accounting, and constraint residuals. | 4 |
| algorithms.proofs.network-scoring | Additive scoring of a Bayesian network. | 2 |
| algorithms.proofs.newton | Newton's method as the general descent skeleton with a Hessian-inverse step size. | 1 |
| algorithms.proofs.noisy-descent | AHoF O38 Noisy Descent: the WRAP pattern that perturbs a base descent step with additive noise. | 3 |
| algorithms.proofs.odd-monitor | Operational Design Domain (ODD) monitoring over exact rationals (AHoF V59). | 1 |
| algorithms.proofs.order-statistic | AHoF empirical rank / order statistic: the count of sample values that fall at or below a threshold, count-at-most t xs = |{ x in xs : x <= t }|, the unnormalized empirical CDF at t that underlies quantile estimation, rank statistics, and Monte-Carlo hit counting. | 4 |
| algorithms.proofs.particle-swarm | AHoF O45 Particle Swarm Optimization: the per-particle velocity and position update over genuinely n-dimensional vector state. | 5 |
| algorithms.proofs.particle-swarm-best-iterate | Finite-horizon best-so-far recurrence and objective monotonicity. | 6 |
| algorithms.proofs.particle-swarm-convex-move | Normalized movement toward a swarm best preserves vector intervals. | 5 |
| algorithms.proofs.particle-swarm-convex-trajectory | Finite normalized consensus trajectories remain inside invariant intervals. | 5 |
| algorithms.proofs.particle-swarm-global-best | Verified finite-swarm global-best selection and best-so-far monotonicity. | 7 |
| algorithms.proofs.particle-swarm-projected-trajectory | Box-projected particle updates and finite-horizon trajectory boundedness. | 6 |
| algorithms.proofs.path-relaxation | AHoF shortest-path edge relaxation (the core step of Bellman-Ford and Dijkstra): when a candidate path of cost `alt` reaches a node whose current best cost is `current`, the tentative distance is relaxed to the smaller of the two, relax current alt = nnrat-min current alt = if (current <= alt) then current else alt using the decidable rational order. | 4 |
| algorithms.proofs.pattern-search | Generalized pattern search over exact rationals: a derivative-free poll that moves to the best of a set of candidate points. | 3 |
| algorithms.proofs.penalty-method | AHoF O48 Penalty Method: the transform that turns a constrained problem into an unconstrained one by folding a penalty on constraint violation into the objective: augmented(x) = objective(x) + rho * penalty(x) where rho is the penalty weight and penalty(x) measures constraint violation (zero when feasible). | 3 |
| algorithms.proofs.powell | AHoF O33 Powell's Method: the conjugate search-direction generated from a cycle of coordinate line minimizations. | 3 |
| algorithms.proofs.prefix-sum | Cumulative sum (prefix-sum / scan): the running totals of a list, cumulative-sum [x0, x1, x2, ...] = [x0, x0+x1, x0+x1+x2, ...]. | 3 |
| algorithms.proofs.reward-to-go | AHoF D47 Reward-to-Go: the future-reward sum used by policy-gradient methods to reduce variance (REINFORCE uses the whole-trajectory return as the weight; reward-to-go replaces it with only the rewards from step t onward). | 4 |
| algorithms.proofs.rmsprop | AHoF O22 RMSProp: the decayed squared-gradient accumulator that adapts the learning rate. | 3 |
| algorithms.proofs.robustness-objective | The robustness-based falsification objective over signed rationals. | 2 |
| algorithms.proofs.sarsa | SARSA on-policy temporal-difference control over signed rationals. | 2 |
| algorithms.proofs.simulated-annealing | AHoF O40 Simulated Annealing: the geometric temperature schedule and the deterministic (greedy-limit) Metropolis acceptance. | 4 |
| algorithms.proofs.sparse-sampling | AHoF D35 Sparse Sampling: the sample-complexity count of the sparse-sampling MDP planner (Kearns-Mansour-Ng). | 4 |
| algorithms.proofs.tournament-selection | AHoF O43 Genetic Algorithm -- tournament selection operator: from a sampled tournament of candidate fitnesses the fittest (maximum) entrant is selected to reproduce. | 3 |
| algorithms.proofs.triangular | AHoF triangular numbers T(n) = 0 + 1 + ... | 4 |
| algorithms.proofs.trust-region | Trust region step acceptance over exact rationals. | 4 |