Implementation map

Finite-horizon pseudo-regret equals the sum over arms of each gap multiplied by its pull count.

A selected successor reward on the canonical generated trajectory inherits the centered conditional MGF bound supplied by its step kernel.

If every index in a nonempty finite family receives an equal geometric confidence share at every time, the outer measure of any time-index failure is at most the total confidence budget.

On one canonical generated action/reward trajectory, every finite arm and every positive successor horizon obeys the existing random-pull-count empirical-mean radius outside an event of outer measure at most the total geometric confidence budget.

On one canonical generated action/reward trajectory, every finite arm and positive successor horizon obeys the existing random-pull-count empirical-mean radius at share delta/((n+1)(n+2))/|A| outside an event of outer measure at most delta.

One horizon-free scheduled UCB policy uses the telescoping per-round confidence share on its own generated finite history. On the same canonical action/reward trajectory measure, one all-time confidence event controls every positive-gap arm at every finite horizon, and each finite horizon has an explicit expected pseudo-regret bound.

The generated-history law, conditional sub-Gaussian MGF, and finite-arm/time empirical-mean event actually required by the scoped ETC and horizon-indexed UCB routes compile through one external Book Map canary; the reusable countable adapter is exposed separately.

The generated ETC policy under finite-arm sub-Gaussian reward laws satisfies the explicit exploration-plus-wrong-commit expected pseudo-regret bound.

The Rat commit oracle used by the measurable generated ETC policy is Mathlib's first-occurrence argmax on Fin K, hence chooses the least encoded arm among tied maxima.

The local canonical ETC chapter route compiles; direct identity with the pinned LML declaration remains a separate cross-toolchain theorem-card route and is not claimed here.

The generated selected-policy UCB action satisfies a textbook-shaped Real pseudo-regret gap-sum bound, including the zero-proxy case.

For the compiled finite-arm sub-Gaussian source, expected pseudo-regret divided by the horizon tends to zero.

For each explicit horizon and confidence budget, one generated pair-trajectory family carries the finite-arm/time confidence event through large-gap and pull-count bounds to finite-arm expected pseudo-regret; the scheduled family has vanishing expected average regret.

Local ordinary-UCB and Real arm-stream one-policy results compile; only literal identity with the pinned upstream declaration remains a separate theorem-card/cross-toolchain gate.

ABRL has compiled local ETC/UCB theorems shaped against the pinned LeanMachineLearning cards, but it does not import or consume the actual upstream Bandits.ETC.regret_le or Bandits.UCB.regret_le declarations.

Clipped inverse-Gram quadratic widths are bounded by a dimension-scaled log-determinant growth term.

The finite-dimensional conditional-MGF and Gaussian-mixture route controls the ridge-estimation error in the regularized matrix norm.

A strict-fold finite-action selector turns ridge estimates and scheduled confidence radii into one measurable history algorithm without a terminal horizon parameter.

A telescoping confidence-budget schedule controls one countable failure event for the generated scalar-ridge policy at every deterministic horizon.

On the same canonical trajectory generated by the horizon-free telescoping policy, one outer-measure event controls the explicit pseudo-regret bound for every finite horizon.

For the separate horizon-indexed fixed-model policy family, the canonical expected pseudo-regret bound is little-o of the horizon, so the corresponding expected average tends to zero.

For the same horizon-free telescoping generated policy, any stopping time bounded by a deterministic horizon has nonnegative expected stopped pseudo-regret bounded by the endpoint budget plus the explicit delta-weighted envelope.

Under an explicit square-integrable finite stopping-time contract, the stopped high-probability pseudo-regret is integrable and receives a second-moment-controlled expectation bound.

When the observed environment-history pair has the canonical prior-likelihood joint law, the canonical posterior kernel is almost everywhere the conditional distribution of the environment given history.

Sampling an environment from the canonical posterior and applying the measurable best-action selector gives the same conditional action law as the posterior best action.

For every round, the successor action on the recursively generated Thompson trajectory conditioned on its own finite history has the posterior-best-action conditional law.

Probability matching transports finite-history scores so generated comparator-relative mean regret splits exactly into selector and selected-action clipped-score terms; it becomes Bayesian regret when the selector is mean-optimal.

The actual recursive trajectory reward coordinates agree almost everywhere with the next-unused-coordinate reward read from the selected arm's latent stream.

Under the explicit pointwise mean-optimal selector, stationary Markov, bounded-mean, and centered sub-Gaussian contracts, the canonical generated Thompson trajectory satisfies E[R_n^Bayes] <= (2K+1)(u-l)+8 sqrt(sigma^2 K n log n).

The stationary local endpoint is complete, but posterior-law producers outside that model and exact upstream compatibility remain separate obligations.

The generated predictable EXP3 process satisfies an explicit square-root expected-regret bound.

For each supplied positive horizon, finite comparator aggregation gives the generated horizon-tuned EXP3 law a best-supported-arm realized-regret tail; changing the horizon changes the parameters and law.

A countable union of indexwise deviation-and-variance events is controlled by the sum of their confidence shares and hence by a caller-supplied total budget.

On one generated EXP3 trajectory law, geometric confidence shares control the joint selected-loss deviation and predictable-variance failures over every positive prefix by one outer budget.

On one fixed generated EXP3 process, the realized selected loss minus its predictable counterpart stays below its geometrically scheduled radius at every positive prefix outside one failure event of outer mass at most delta.

For one fixed generated EXP3 process and one supported comparator, every positive-prefix predictable-regret failure is covered by a single geometrically budgeted event.

For one generated EXP3 process and one supported comparator, the realized selected-loss regret at every positive prefix is controlled by the sum of the predictable-regret and realized-deviation schedules outside one event of outer mass at most delta.

The best-arm realized-regret tail is controlled with the supplied sparsity-failure probability left explicit.

IID probability arm laws with exact model means and positive non-best gaps yield a logarithmic reciprocal-gap regret bound.

A measurable predictable corruption model receives an internally selected refined or logarithmic regret bound.

Predictable-environment regret to the actual moving best arm is bounded by the fixed-comparator route plus an explicit mean-drift penalty.

A change-point schedule built from population-mean switches generates a single restart trajectory whose expected dynamic regret is bounded by the square-root switch-count rate under the route's support assumptions.

Finite-horizon MDP data, measurable Markov policies, recursive value functions, optimal Bellman operators, and an attaining optimal policy are formalized locally.

A Markov policy's expected regret equals the occupancy-weighted Bellman optimality gap and is nonnegative; the optimal policy has zero regret.

With the explicit path-support, bounded-mean, sub-Gaussian, scheduling, and Standard Borel contracts, both the failure budget and average realized behavior-regret envelope tend to zero across windows.

For each fixed threshold index and horizon greater than four, the genuine uncapped Mathlib hittingAfter has an L2 round count under the exact generated causal source.

For every fixed inverse-sqrt threshold index and horizon greater than four, the exact average realized behavior-regret process stopped at the uncapped hit is integrable and its integral is at most that threshold.

One generated adaptive process now carries exact aggregate transition numerators and visit denominators, a previous-Q clipped recurrent planner, a strict-prefix measurable policy, joint same-source singleton-Bernstein and optimal-tail confidence, Bellman optimism, raw generated episode pseudo-regret, actual-count charge summation, and a generated-filtration Bellman martingale.

On the recurrent source's own trajectory measure, the probability that raw K-episode policy-value pseudo-regret exceeds 20 H sqrt(H) L sqrt(S A K) + 250 H^2 S^2 A L^2 is at most delta. The matching integrable expectation is at most that bound plus K H delta.

An adapted natural-valued spending process reaches a fixed budget at a stopping time.

Stopping-time and several positive-cost budget adapters compile, but there is no full resource process, feasibility invariant, primal-dual comparison, and BwK regret theorem.

One horizon-free measurable policy uses the actual Bernoulli-KL confidence-set supremum on its generated reward history. On the same canonical trajectory measure, a telescoping all-time confidence event controls every positive-gap arm at every finite horizon and yields a conservative finite-time expected pseudo-regret bound.

The Chapter 13 conversion window compiles explicit ENNReal worst-case/minimax semantics, a source-shaped least-explored alternative-arm theorem from the exact expected pull budget, and quantitative deterministic two-environment regret algebra whose cross-law pull discrepancy remains a visible error premise.

The scoped §14.2 spine compiles extended-real measure relative entropy with explicit absolute-continuity, integrability, and singular branches; event-level Bernoulli data processing; binary endpoint analysis; and the unconditional Bretagnolle–Huber inequality in the exact D(P,Q) direction.

For real means mu and nu, the project constructs the unit-variance Gaussian arm laws, identifies their log Radon–Nikodym derivative under the first law, proves its integrability, and derives the exact extended-real identity D(N(mu,1),N(nu,1))=(mu-nu)^2/2. The changed-arm cost, source gap, exact information exponent one half, and unit-cube gap upper bound also compile.

For finite arms, a countably generated reward space, arbitrary stationary Markov arm laws, and one common randomized history policy, the directed KL between the two canonical finite history laws equals the finite sum of first-law realized expected pull counts times the corresponding directed arm KL. The proof includes singular fibres and infinite arm KL through an extended-real conditional-kernel chain rule.

The project states Definition 16.1's every-environment/every-positive-real-power consistency interface, proves closure and eventual power/log-growth consequences for two regret sequences, defines the source extended-real d_inf with strict confusing alternatives in the original-to-alternative KL direction, and computes an exact unit-Gaussian perturbed-alternative upper bound.

The source-frozen endpoints are Theorem 16.2's unstructured-class liminf regret constant, Lemma 16.3's one-arm finite-time expected-pull inequality, and Theorem 16.4's unit-Gaussian local-envelope positive-part lower bound. No local declaration is presented as any of these terminals.

The project freezes the exact stochastic and adversarial Chapter 17 threshold surfaces, compiles Claim 17.5's first-moment deterministic-witness argument with integrability explicit, proves the 2delta-minus-delta event subtraction, and proves the deterministic quarter-horizon algebra following Eq. (17.8).

The source-frozen endpoints are Theorem 17.1, Corollaries 17.2–17.3, Theorem 17.4, Claims 17.6–17.7, and construction-level Eq. (17.8). No local declaration is presented as any of these terminals.

For k-armed unit-variance Gaussian bandits with mean vectors in the unit cube, the source states a universal-constant minimax lower bound of order sqrt(k n) for k greater than one and n at least k; Chapter 15 now freezes the exact proof target and compiles the Gaussian arm KL dependency, but BanditRLlib makes no local compiled-terminal claim.

For the frozen NeurIPS 2025 delayed best-of-both-worlds source, the library formalizes strict pre-action observability, outstanding rounds, their exact finite partition, paper-style end-of-round missing-feedback counts, and the explicit one-based indexing bridge. This is deterministic accounting, not a regret theorem.

The learner view exposes past actions and exactly the losses available before the next action. Observation-equivalent hidden worlds are indistinguishable to any typed causal decision rule, and the set-level update processes precisely the newly observed rounds. A separate downstream layer now constructs a one-round measure-valued rule; a measurable recursive policy kernel and the paper's ordered state updates remain open.

Algorithm 5's equal residual allocation over a nonempty active set is normalized and coordinatewise nonnegative whenever the inactive coordinates are nonnegative and carry at most unit mass. No claim is made that the unformalized EAP state maintains those premises.

Algorithm 5 lines 7--8 compile as a source-exact elimination snapshot. The deterministic core of Lemma D.9 proves that an explicit optimal-arm-survival certificate closes the nonempty-active premise for line 15. With EAP's still-explicit nonnegativity and mass premises, the resulting vector induces a genuine one-round probability measure, and every allocation rule typed on the causal view returns the same measure in observation-equivalent hidden worlds. The source-shaped good-event projection that constructs the certificate is compiled separately; this milestone is not the full lemma, a measurable history kernel, or a regret endpoint.

A source-shaped confidence snapshot defines ucbStar as the finite-arm infimum of the two upper-confidence surfaces used in the paper. Its elimination projection of Definition D.1 derives muStar <= ucbStar rather than assuming that inequality as an independent certificate, constructs the deterministic Lemma-D.9 survival certificate, and transports any externally supplied complement-good-event probability bound to an optimal-arm-elimination bound. Corollary D.8's six-event union assembly is compiled separately; the full Definition-D.1 event and the D.2--D.7 component concentration/counting producers remain open.

Six explicitly named failure components represent the clauses discharged by source Lemmas D.2--D.7. The compiled Corollary-D.8 layer proves that three 1/T^2 budgets and three 1/T budgets combine into the paper's deliberately loose 9/T complement-good-event bound, then transports a recorded full-event-to-elimination projection through the compiled D.9 consumer to bound optimal-arm elimination. The six concentration/counting bounds and the semantic projection are hypotheses, not claimed source theorems.

Lean proves that the source inverse-square-root empirical width is antitone in a positive pull count and gives both a normalized count-one/count-four witness and a literal T=4 witness against the printed reverse transport. It also proves the exact source-shaped small-count implication count <= 192 log T -> 1 <= 10 width. A branched active-arm consumer uses current-UCB and the optimal-to-later factor-three edge only in the large-count branch, while the small-count branch uses bounded means plus an explicit source-width/count certificate. Together with an explicit later-to-earlier factor-ten width premise, this yields a conditional same-snapshot factor-20 consumer without transport to a later elimination snapshot. The recursive trajectory does not yet produce the branch, source-width/count, or factor-ten certificates. The earlier explicit four-edge consumer remains for comparison. These 19 declarations do not verify or refute source Lemmas D.10/D.12, main-text Lemma 4.2, or Theorem 4.1.

The exact NeurIPS 2025 source is hash-frozen, a same-algorithm multi-regime contract compiles, and 107 named source-audit declarations compile across accounting, causality, processing, allocation, elimination, good-event projection/union assembly, the one-round action law, and a 19-declaration D.10/D.12 diagnostic/conditional/repair layer. That layer includes a literal T=4 direction witness, the exact source-shaped small-count scalar implication, and a large/small-count conditional same-snapshot factor-20 skeleton. It does not verify or refute source Lemmas D.10/D.12, main-text Lemma 4.2, or Theorem 4.1 because the recursive branch/count/width producers and same-prefix factor-ten comparison remain open. BanditRLlib does not yet implement the full Delayed SAPO trajectory, prove the D.2--D.7 component bounds on that trajectory, or prove either regret endpoint.

Version 2 reuses 30 frozen source cases while balancing 75 source-faithful and 75 injected-drift target-replicate triplets across compile-only, source-aware blueprint, and full ABRL conditions. Both variants use one matched field/value template, with a frozen text-only leakage diagnostic. The result-free protocol and component-tested code specify a pre-audit common workspace, opaque identifiers, content-addressed sealing, an agent-adapter interface, workflow-artifact presence/hash records, blind grading packets, and source/target-aware analysis with multiplicity-controlled secondary endpoints. Neutral replay is split into a host controller that never executes Lean, a canonical Docker launcher, a trusted in-image controller, and a restricted Lean worker. The sandbox receives only a pristine base snapshot, submitted patch, public declaration names, expected file hashes, and opaque/hash bindings; the complete sealed pack, operator metadata, source bank, condition, variant, and ground truth are excluded. Runtime binding covers the allowlisted Docker executable, version/daemon/signature-or-package ledger, image recipe/SBOM, exact argv, and actual launcher/controller/inner bytes. A provenance-bound multi-stage builder now derives the cache-complete image context from the exact common pre-audit Git snapshot, excludes evaluation and operator data, runs the full Lean and Tests targets, byte-manifests the cache, keeps builder-stage source out of the final image, and emits an image/toolchain/cache SBOM plus sealed provenance sidecars. A result-free Linux CI candidate build then produced an unpublished cache-complete image, a 121,277-file cache manifest, and matching build-input/log/SBOM hashes after an offline Lean 4.29.1 / Lake 5.0.0-src+f72c35b worker probe. The candidate image existed only on the ephemeral runner and is not a frozen production image or isolation evidence. The launcher verifies the manifest extracted from a digest-pinned image, the inner checker verifies every cached file, and the already restricted worker copies the seed into the per-run tmpfs replay. A real provider image, final published checker image, passed seven-probe checker isolation report, final seal, preregistered real-infrastructure smoke, and all primary runs remain pending; no model run or formalization outcome is reported.