Compiled endpoints and named gaps
Progress means a declaration compiled under its exact hypotheses. Route completion means the advertised mathematical target is reached. These are tracked separately.
pie showData title Implementation-map milestones (not a percentage of all mathematics) "Compiled local endpoint" : 60 "Partial route" : 4 "Planned" : 1 "Blocked" : 5 "Stated, proof incomplete" : 0
The count is auditable in website/content/results.json. It is not an estimate of the percentage of the field completed.
Finite-horizon pseudo-regret equals the sum over arms of each gap multiplied by its pull count.
Lean: BanditRLProof.pseudoRegret_eq_finset_sum_gap_mul_pullCount
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/RegretDecomposition.lean
A selected successor reward on the canonical generated trajectory inherits the centered conditional MGF bound supplied by its step kernel.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/ConditionalRewardLawSource.lean
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.
Lean: BanditRLProof.Concentration.measure_iUnion_iUnion_fintype_le_tsum_of_uniform · BanditRLProof.Concentration.measure_iUnion_iUnion_fintype_le_delta_of_geometricConfidenceShare
Remaining: Each ETC, UCB, or RL consumer must still supply its per-time, per-index tail events and model-specific law assumptions.
Evidence: BanditRLProof/ConcentrationFintypeGeometricAllTime.lean
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.
Lean: BanditRLProof.ConditionalExpectationReward.successorArmEmpiricalMeanFintypeGeometricAllTimeBadEvent · BanditRLProof.ConditionalExpectationReward.actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_fintype_geometricAllTime_abs_tail_ennreal_delta_trajMeasure
Remaining: The ordinary-UCB chapter uses its exact finite-arm/time confidence producer. A fixed-policy anytime UCB consumer for this stronger geometric event remains a separate extension.
Evidence: BanditRLProof/ConditionalRewardPartialTrajectoryGeometricAllTime.lean
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.
Lean: BanditRLProof.Concentration.tsum_ofReal_telescopingConfidenceShare · BanditRLProof.Concentration.measure_iUnion_iUnion_fintype_le_delta_of_telescopingConfidenceShare · BanditRLProof.ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent · BanditRLProof.ConditionalExpectationReward.actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_fintype_telescopingAllTime_abs_tail_ennreal_delta_trajMeasure
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/ConditionalRewardPartialTrajectoryTelescopingAllTime.lean
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.
Lean: BanditRLProof.UCB.selectedPolicySuccessorTelescopingHistoryPolicy · BanditRLProof.UCB.selectedPolicySuccessorTelescopingPairHistory_eq_finitePairHistoryOfTrace · BanditRLProof.UCB.measure_selectedPolicySuccessorTelescoping_allTimeBadEvent_le_trajMeasure · BanditRLProof.UCB.selectedPolicySuccessorTelescoping_allHorizonPullCount_of_not_badEvent · BanditRLProof.UCB.lintegral_ofReal_pseudoRegret_selectedPolicySuccessorTelescoping_le_trajMeasure
Remaining: The finite-time expectation keeps the explicit T times delta failure contribution; fixed-delta expected-average consistency is not claimed. The compiled bounded KL-UCB extension is mapped separately; literal pinned-LML identity remains cross-toolchain work.
Evidence: Tests/UCBFixedPolicyTelescopingAnytimeRegretCanary.lean
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.
Lean: BanditRLProof.ConditionalExpectationReward.historyStepKernelFamily_generatedActionPartialTrajectoryPairLawSource_trajMeasure · BanditRLProof.ConditionalExpectationReward.historyStepKernelFamily_centeredReward_succ_hasCondSubgaussianMGF_trajMeasure · BanditRLProof.ConditionalExpectationReward.actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_finiteArmTime_abs_tail_ennreal_delta_trajMeasure
Remaining: No missing step recorded for this milestone.
Evidence: Tests/BookMapChaptersTwoToFourCanary.lean
The generated ETC policy under finite-arm sub-Gaussian reward laws satisfies the explicit exploration-plus-wrong-commit expected pseudo-regret bound.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Algorithms/ETCFiniteArmRewardLaw.lean
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.
Lean: BanditRLProof.ETC.argmaxCommitOracle_argmax_finRange · BanditRLProof.ETC.argmaxCommitOracle_encode_le_of_score_le
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Algorithms/ETCArgmaxOracle.lean
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.
Remaining: Direct imported-LML symbol and toolchain identity remains cross-toolchain work.
Evidence: tasks/BRL-ETC-PORT-001.md
The generated selected-policy UCB action satisfies a textbook-shaped Real pseudo-regret gap-sum bound, including the zero-proxy case.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Algorithms/UCBFiniteArmSubGaussianRewardLaw.lean
For the compiled finite-arm sub-Gaussian source, expected pseudo-regret divided by the horizon tends to zero.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Algorithms/UCBFiniteArmSubGaussianSampledAsymptotics.lean
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.
Lean: BanditRLProof.UCB.measure_selectedPolicySuccessorLargeGapEvent_generatedUCB_le_ennreal_delta_actionRewardTrajMeasure_centeredKernel · BanditRLProof.UCB.measure_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_gt_explicitPullThreshold_le_ennreal_delta_actionRewardTrajMeasure_centeredKernel · BanditRLProof.UCB.selectedPolicySuccessorFiniteArmSubgaussianExpectedPseudoRegret_nonneg_and_le · BanditRLProof.UCB.selectedPolicySuccessorFiniteArmSubgaussianExpectedAveragePseudoRegret_tendsto_zero
Remaining: This is a horizon-indexed policy family, not a single fixed-policy anytime UCB theorem.
Evidence: Tests/BookMapChaptersTwoToFourCanary.lean
Clipped inverse-Gram quadratic widths are bounded by a dimension-scaled log-determinant growth term.
Lean: BanditRLProof.OFUL.sum_range_min_prefix_update_le_two_trace_average_log
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/OFULEllipticalPotential.lean
The finite-dimensional conditional-MGF and Gaussian-mixture route controls the ridge-estimation error in the regularized matrix norm.
Lean: BanditRLProof.OFUL.fixedDirectionCompensatedScore_hasMGFUpperBoundAt · BanditRLProof.OFUL.measure_finiteHorizonRidgeEstimate_error_matrixNorm_gt_confidenceRadius_le
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/OFULSelfNormalizedConfidence.lean; BanditRLProof/OFULConfidenceEllipsoid.lean
A strict-fold finite-action selector turns ridge estimates and scheduled confidence radii into one measurable history algorithm without a terminal horizon parameter.
Lean: BanditRLProof.OFUL.finiteHistoryTelescopingScalarRidgeOptimisticAlgorithm
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/OFULScheduledAllTimeConfidence.lean
A telescoping confidence-budget schedule controls one countable failure event for the generated scalar-ridge policy at every deterministic horizon.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/OFULScheduledAllTimeConfidence.lean
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.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/OFULScheduledAllHorizonHighProbabilityRegretRate.lean
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.
Lean: BanditRLProof.OFUL.canonicalStandardExpectedAveragePseudoRegret_tendsto_zero
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/OFULExpectedRegretConsistency.lean
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.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/OFULScheduledBoundedStoppingTimeExpectedRegret.lean
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.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/OFULScheduledUnboundedStoppingTimeExpectedRegretExactMoment.lean
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.
Lean: BanditRLProof.PosteriorKernel.canonicalPosterior_kernel_ae_eq_condDistrib_of_pair_map_eq
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/PosteriorKernel.lean
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.
Lean: BanditRLProof.Thompson.canonicalSampler_condDistrib_action_ae_eq_bestAction
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Algorithms/ThompsonCanonicalSampler.lean
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.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Algorithms/ThompsonRecursiveSampler.lean
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.
Lean: BanditRLProof.Thompson.integral_trajectoryBayesMeanRegret_eq_add_historyScore · BanditRLProof.Thompson.integral_trajectoryBayesMeanRegret_eq_add_clippedUCB
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Algorithms/ThompsonBayesRegretDecomposition.lean; BanditRLProof/Algorithms/ThompsonClippedUCBScore.lean
The actual recursive trajectory reward coordinates agree almost everywhere with the next-unused-coordinate reward read from the selected arm's latent stream.
Lean: BanditRLProof.Thompson.canonicalLatentArmStreamTrajectory_reward_eq_rewardFromArmStream_ae
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Algorithms/ThompsonStationaryReward.lean
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).
Lean: BanditRLProof.Thompson.IsOptimalMeanSelector · BanditRLProof.Thompson.stationaryLatentArmStreamCanonicalTrajectoryMeasure_integral_trajectoryBayesMeanRegret_le
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Algorithms/ThompsonStationaryReward.lean
The generated predictable EXP3 process satisfies an explicit square-root expected-regret bound.
Lean: BanditRLProof.Exp3.sampledPredictable_expectedRegret_le_four_mul_sqrt
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Exp3ExpectedRegret.lean
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.
Lean: BanditRLProof.Exp3.sampledPredictable_allHorizonBernsteinSquareBestArmRealizedRegret_tail
Remaining: This is not one horizon-free policy with a simultaneous confidence event over all horizons.
Evidence: Tests/BookMapChaptersSevenAndEightCanary.lean; BanditRLProof/Exp3MixedSquareBernsteinRealizedBestArmAllHorizon.lean
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.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/ConcentrationQuadraticScheduled.lean; tasks/CONCENTRATION-QUADRATIC-COUNTABLE-SCHEDULED-TAIL.md
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.
Lean: BanditRLProof.Exp3.measure_sampledPredictableRealizedDeviationAllTimeFailureSet_le
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Exp3RealizedPredictableVarianceAllTime.lean; tasks/EXP3-REALIZED-PREDICTABLE-VARIANCE-GEOMETRIC-ALL-TIME-TAIL.md
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.
Lean: BanditRLProof.Exp3.measure_sampledRealizedDeviationGeometricAllTimeFailureSet_le
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Exp3RealizedDeviationAllTime.lean; tasks/EXP3-REALIZED-DEVIATION-GEOMETRIC-ALL-TIME-TAIL.md
For one fixed generated EXP3 process and one supported comparator, every positive-prefix predictable-regret failure is covered by a single geometrically budgeted event.
Lean: BanditRLProof.Exp3.measure_sampledPredictableRegretGeometricAllTimeFailureSet_le
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Exp3PredictableRegretAllTime.lean; tasks/EXP3-PREDICTABLE-REGRET-GEOMETRIC-ALL-TIME-TAIL.md
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.
Lean: BanditRLProof.Exp3.sampledTrajectoryRealizedRegret_eq_predictableRegret_add_realizedDeviation · BanditRLProof.Exp3.measure_sampledRealizedRegretGeometricAllTimeFailureSet_le
Remaining: The process parameters eta and gamma and the comparator are fixed across prefixes. The theorem is not a horizon-varying tuned sublinear all-time guarantee, a best-arm minimum, or an ideal EXP3.P theorem.
Evidence: Tests/Basic.lean; BanditRLProof/Exp3RealizedRegretAllTime.lean; tasks/EXP3-REALIZED-REGRET-GEOMETRIC-ALL-TIME-TAIL.md
The best-arm realized-regret tail is controlled with the supplied sparsity-failure probability left explicit.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/Exp3MixedSquarePredictableVarianceSparseLossRealizedDoublePathwiseVarianceProbabilisticSparsityBestArmAllHorizon.lean
IID probability arm laws with exact model means and positive non-best gaps yield a logarithmic reciprocal-gap regret bound.
Lean: BanditRLProof.Tsallis.integral_sampledScheduledHalfTsallisFiniteArmIIDRewardLawRegret_le_log
Remaining: No missing step recorded for this milestone.
Evidence: Tests/BookMapChaptersSevenAndEightCanary.lean; BanditRLProof/TsallisFiniteArmIIDRewardLaw.lean
A measurable predictable corruption model receives an internally selected refined or logarithmic regret bound.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/TsallisFiniteArmIIDHistoryAdaptiveExpectedCorruptedRewardLaw.lean
Predictable-environment regret to the actual moving best arm is bounded by the fixed-comparator route plus an explicit mean-drift penalty.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/TsallisFiniteArmIndependentDriftingMeanDynamicRegret.lean
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.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/TsallisOracleRestartGlobalMeanSwitchCount.lean
Finite-horizon MDP data, measurable Markov policies, recursive value functions, optimal Bellman operators, and an attaining optimal policy are formalized locally.
Lean: BanditRLProof.FiniteHorizonRL.MDP · BanditRLProof.FiniteHorizonRL.MDP.optimalValueAt_dominates_and_is_attained
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/RL/FiniteHorizonMDP.lean; BanditRLProof/RL/FiniteHorizonOptimality.lean
A Markov policy's expected regret equals the occupancy-weighted Bellman optimality gap and is nonnegative; the optimal policy has zero regret.
Lean: BanditRLProof.FiniteHorizonRL.MarkovPolicy.expectedRegret_eq_occupancyGapRemaining · BanditRLProof.FiniteHorizonRL.MDP.expectedRegret_eq_occupancyGap_nonneg_and_optimalPolicy_zero
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/RL/FiniteHorizonOccupancyRegret.lean
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.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/RL/FiniteHorizonAdaptiveStochasticRewardCumulativeDecayingExplorationRegularityClosedConsistency.lean
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.
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/RL/FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterSquareIntegrableFiniteStoppingTime.lean
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.
Remaining: No missing step recorded for this milestone.
Evidence: tasks/RL-FINITE-HORIZON-NATURAL-CAUSAL-INVERSE-SQRT-THRESHOLD-UNBOUNDED-HITTINGAFTER-INTEGRABLE-EXPECTED-UPPER-BOUND.md
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.
Lean: BanditRLProof.FiniteHorizonRL.sum_adaptiveCumulativeAggregateTransitionCountAt_eq_visitCountAt · BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.clippedQRemaining_of_aggregateVisitCount_pos · BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_policyAt_succ · BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_simultaneousTransitionFailureEvent_le_fifth · BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.recurrentQTableOfTrajectory_dominatesOptimal · BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.recurrentSource_generatedSuccessorPseudoRegret_le_charge_add_innovation · BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.totalGeneratedPairCharge_le_explicit · BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_bellmanInnovation_sum_ge_threshold_le_fifth
Remaining: No missing step recorded for this milestone.
Evidence: Tests/BookMapChapterNineCanary.lean
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.
Lean: BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_cumulativeEpisodePseudoRegret_gt_canonicalRegretBound_le · BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.integral_cumulativeEpisodePseudoRegret_recurrentSource_le_canonicalRegretBound_add_failure
Remaining: Bernstein/variance-aware minimax UCB-VI leading-rate theorem. Stochastic-reward and realized sampled-return UCBVI terminals. Posterior-sampling, model-free, and continuous-space RL extensions.
Evidence: Tests/BookMapChapterNineCanary.lean
An adapted natural-valued spending process reaches a fixed budget at a stopping time.
Lean: BanditRLProof.Budget.isStoppingTime_budgetExhaustionTime_of_adapted
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/BudgetStoppingTime.lean
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.
Lean: BanditRLProof.KLUCB.bernoulliKL · BanditRLProof.KLUCB.index · BanditRLProof.KLUCB.historyPolicy · BanditRLProof.KLUCB.pairHistory_eq_finitePairHistoryOfTrace · BanditRLProof.KLUCB.generatedIndexAt_le_selected_of_K_le · BanditRLProof.KLUCB.measure_generatedKLAllTimeBadEvent_le_trajMeasure · BanditRLProof.KLUCB.allHorizonPullCount_of_not_badEvent · BanditRLProof.KLUCB.lintegral_ofReal_pseudoRegret_generatedKLUCBBounded_le_trajMeasure
Remaining: The finite-time conservative route assumes AE [0,1] rewards and means in [margin,1-margin], and retains T times delta. Sharp KL-Chernoff concentration, the Garivier-Cappe leading constant, and asymptotic optimality are not claimed.
Evidence: Tests/KLUCBGeneratedRegretCanary.lean
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.
Lean: BanditRLProof.LowerBounds.worstCaseExpectedRegret · BanditRLProof.LowerBounds.minimaxExpectedRegret · BanditRLProof.LowerBounds.expectedRegret_le_worstCaseExpectedRegret · BanditRLProof.LowerBounds.minimaxExpectedRegret_le_worstCaseExpectedRegret · BanditRLProof.LowerBounds.le_minimaxExpectedRegret · BanditRLProof.LowerBounds.exists_alternative_le_average · BanditRLProof.LowerBounds.alternativeExpectedPullBudget_le · BanditRLProof.LowerBounds.exists_leastExploredAlternative · BanditRLProof.LowerBounds.baseEnvironmentRegret · BanditRLProof.LowerBounds.changedEnvironmentRegretLowerBound · BanditRLProof.LowerBounds.max_base_changed_regretLowerBound_ge_half_sub_error · BanditRLProof.LowerBounds.max_base_changed_regretLowerBound_ge_half
Remaining: The Chapter 14 event-testing foundation and Chapter 15 same-policy adaptive-history KL identity compile. The source-stated Gaussian minimax Theorem 13.1 remains blocked on the Chapter 15 regret/event consumer, constant assembly, and caller-free terminal.
Evidence: BanditRLProof/LowerBounds/BasicIdeas.lean; Tests/TextbookPartIVChapter13Canary.lean
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.
Lean: BanditRLProof.LowerBounds.relativeEntropy · BanditRLProof.LowerBounds.relativeEntropy_of_absolutelyContinuous_of_integrable · BanditRLProof.LowerBounds.relativeEntropy_of_probability_absolutelyContinuous_of_integrable · BanditRLProof.LowerBounds.relativeEntropy_eq_top_of_not_absolutelyContinuous · BanditRLProof.LowerBounds.relativeEntropy_ne_top_iff · BanditRLProof.LowerBounds.bernoulliRelativeEntropy · BanditRLProof.LowerBounds.rnDeriv_restrict_restrict · BanditRLProof.LowerBounds.relativeEntropy_restrict_add_compl · BanditRLProof.LowerBounds.bernoulliKLCore_event_le · BanditRLProof.LowerBounds.exp_neg_half_bernoulliKLCore_le_affinity · BanditRLProof.LowerBounds.half_binaryAffinity_sq_le_eventError · BanditRLProof.LowerBounds.binaryBretagnolleHuberCore · BanditRLProof.LowerBounds.bretagnolleHuberScale · BanditRLProof.LowerBounds.bretagnolleHuberScale_nonneg · BanditRLProof.LowerBounds.binaryBretagnolleHuber · BanditRLProof.LowerBounds.bernoulliRelativeEntropy_event_le · BanditRLProof.LowerBounds.bretagnolleHuberScale_antitone · BanditRLProof.LowerBounds.bretagnolleHuber
Remaining: Entropy, Huffman coding, and optimal source-coding results from §14.1 are pedagogically mapped but not formalized by this lower-bound gate. The full arbitrary-sub-sigma-algebra data-processing result in Exercise 14.10 is not claimed; the event/binary specialization is compiled. The adaptive same-policy bandit-history divergence decomposition is a Chapter 15 target, not a Chapter 14 theorem.
Evidence: BanditRLProof/LowerBounds/InformationTheory.lean; Tests/TextbookPartIVChapter14Canary.lean
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.
Lean: BanditRLProof.LowerBounds.unitGaussianArm · BanditRLProof.LowerBounds.unitGaussianBandit · BanditRLProof.LowerBounds.log_gaussianPDFReal_div_gaussianPDFReal_one · BanditRLProof.LowerBounds.llr_gaussianReal_one_ae · BanditRLProof.LowerBounds.integrable_llr_gaussianReal_one · BanditRLProof.LowerBounds.klDiv_gaussianReal_one · BanditRLProof.LowerBounds.klDiv_unitGaussianArm_zero_two_mul · BanditRLProof.LowerBounds.gaussianMinimaxGap · BanditRLProof.LowerBounds.gaussianMinimaxGap_sq · BanditRLProof.LowerBounds.gaussianMinimaxGap_informationExponent_eq_half · BanditRLProof.LowerBounds.gaussianMinimaxGap_le_half
Remaining: Theorem 15.2's regret/event bridge, caller-free 1/27 minimax terminal, and minimax corollary remain blocked; this compiled arm-level slice does not prove them.
Evidence: BanditRLProof/LowerBounds/Minimax.lean; Tests/TextbookPartIVChapter15Canary.lean; tasks/TEXTBOOK-PART-IV-CHAPTER-15-MINIMAX-LOWER-BOUNDS-SPINE.md
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.
Lean: BanditRLProof.LowerBounds.klDiv_compProd_same_left_eq_lintegral_klDiv_of_measurable · BanditRLProof.LowerBounds.klDiv_historyStep_samePolicy_eq_iterated_lintegral_armKL_general · BanditRLProof.LowerBounds.canonicalBanditHistoryMeasure · BanditRLProof.LowerBounds.canonicalBanditHistoryMeasure_succ · BanditRLProof.LowerBounds.finiteHistoryPullCountENNReal · BanditRLProof.LowerBounds.canonicalRealizedExpectedPullCountThrough · BanditRLProof.LowerBounds.canonicalRealizedExpectedPullCountThrough_eq_expectedPullCountThrough · BanditRLProof.LowerBounds.klDiv_canonicalBanditHistoryMeasure_eq_sum_realizedExpectedPullCount_mul_armKL · BanditRLProof.LowerBounds.banditHistoryRelativeEntropy_eq_expectedPulls_sum
Remaining: The local inclusive-round index lastRound represents lastRound+1 observations; later source consumers must preserve that convention explicitly. This identity does not prove the Gaussian regret event, the 1/27 constant assembly, Theorem 15.2, or later Chapter 16–17 terminals.
Evidence: BanditRLProof/LowerBounds/ConditionalKernelKL.lean; BanditRLProof/LowerBounds/BanditHistoryKL.lean; Tests/TextbookPartIVChapter15Canary.lean
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.
Lean: BanditRLProof.LowerBounds.IsConsistentRegret · BanditRLProof.LowerBounds.IsConsistentPolicyOver · BanditRLProof.LowerBounds.IsConsistentRegret.add · BanditRLProof.LowerBounds.IsConsistentRegret.eventually_add_le_rpow · BanditRLProof.LowerBounds.IsConsistentRegret.eventually_log_add_div_log_le · BanditRLProof.LowerBounds.divergenceInfimum · BanditRLProof.LowerBounds.divergenceInfimum_le · BanditRLProof.LowerBounds.parametricDivergenceInfimum · BanditRLProof.LowerBounds.parametricDivergenceInfimum_le · BanditRLProof.LowerBounds.unitGaussianDivergenceInfimum · BanditRLProof.LowerBounds.unitGaussianDivergenceInfimum_le_perturbed
Remaining: The exact Gaussian d_inf equality still needs its infimum lower bound, epsilon-to-zero argument, and extended-real branch audit. The one-arm expected-pull information constraint must instantiate the compiled Chapter 15 history identity in Chapter 16's event and asymptotic route. Theorem 16.2, Lemma 16.3, and Theorem 16.4 remain blocked; this generic analytic slice does not prove them.
Evidence: BanditRLProof/LowerBounds/InstanceDependent.lean; Tests/TextbookPartIVChapter16Canary.lean; tasks/TEXTBOOK-PART-IV-CHAPTER-16-INSTANCE-DEPENDENT-LOWER-BOUNDS-SPINE.md
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).
Lean: BanditRLProof.LowerBounds.tailAtLeast · BanditRLProof.LowerBounds.stochasticHighProbabilityThreshold · BanditRLProof.LowerBounds.stochasticMinimaxHighProbabilityThreshold · BanditRLProof.LowerBounds.adversarialHighProbabilityThreshold · BanditRLProof.LowerBounds.exists_tailMass_ge_of_integral_ge · BanditRLProof.LowerBounds.exists_cdfTail_ge_of_integral_ge · BanditRLProof.LowerBounds.measureReal_diff_ge_delta · BanditRLProof.LowerBounds.adversarialRegretLowerExpression · BanditRLProof.LowerBounds.adversarialRegretLowerExpression_ge_quarter · BanditRLProof.LowerBounds.randomRegret_ge_quarter_of_clippingDecomposition
Remaining: The stochastic threshold definitions and compiled same-policy adaptive-history KL identity do not yet supply Theorem 17.1's tail-event consumer. The event and deterministic algebra leaves do not construct the clipped-normal reward-matrix law or prove Claims 17.6–17.7 or Eq. (17.8). Only Claim 17.5's first-moment content is a compiled source claim; all other Chapter 17 source terminals remain blocked.
Evidence: BanditRLProof/LowerBounds/HighProbability.lean; Tests/TextbookPartIVChapter17Canary.lean; tasks/TEXTBOOK-PART-IV-CHAPTER-17-HIGH-PROBABILITY-LOWER-BOUNDS-SPINE.md
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.
Lean: BanditRLProof.DelayedFeedback.observedBefore · BanditRLProof.DelayedFeedback.outstandingAt · BanditRLProof.DelayedFeedback.observedBefore_disjoint_outstandingAt · BanditRLProof.DelayedFeedback.observedBefore_union_outstandingAt · BanditRLProof.DelayedFeedback.card_observedBefore_add_card_outstandingAt · BanditRLProof.DelayedFeedback.outstandingCount · BanditRLProof.DelayedFeedback.maxOutstandingBeforeThrough · BanditRLProof.DelayedFeedback.outstandingCount_le_round · BanditRLProof.DelayedFeedback.outstandingCount_le_maxOutstandingBeforeThrough · BanditRLProof.DelayedFeedback.oneBasedDelayShift · BanditRLProof.DelayedFeedback.paperMissingAtEnd · BanditRLProof.DelayedFeedback.paperMissingAtEnd_eq_outstandingAt_oneBasedDelayShift · BanditRLProof.DelayedFeedback.paperMissingCount · BanditRLProof.DelayedFeedback.paperMissingCount_eq_outstandingCount_oneBasedDelayShift · BanditRLProof.DelayedFeedback.paperMissingCount_le_round · BanditRLProof.DelayedFeedback.paperSigmaMaxThrough · BanditRLProof.DelayedFeedback.paperMissingCount_le_paperSigmaMaxThrough
Remaining: No missing step recorded for this milestone.
Evidence: BanditRLProof/DelayedFeedback/Accounting.lean; Tests/DelayedFeedbackPaperAuditCanary.lean; research-wiki/papers/neurips-2025-delayed-bobw-audit.md
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.
Lean: BanditRLProof.DelayedFeedback.ActionTimeView · BanditRLProof.DelayedFeedback.ActionTimeView.ext · BanditRLProof.DelayedFeedback.actionTimeViewAt · BanditRLProof.DelayedFeedback.CausalDecisionRule · BanditRLProof.DelayedFeedback.actionTimeViewAt_pastAction_of_lt · BanditRLProof.DelayedFeedback.actionTimeViewAt_pastAction_of_not_lt · BanditRLProof.DelayedFeedback.actionTimeViewAt_observedLoss_of_mem · BanditRLProof.DelayedFeedback.actionTimeViewAt_observedLoss_of_not_mem · BanditRLProof.DelayedFeedback.actionTimeViewAt_outstanding_loss_hidden · BanditRLProof.DelayedFeedback.actionTimeViewAt_eq_of_observation_equivalent · BanditRLProof.DelayedFeedback.causalDecision_eq_of_observation_equivalent · BanditRLProof.DelayedFeedback.newlyObservedBefore · BanditRLProof.DelayedFeedback.observedBefore_mono · BanditRLProof.DelayedFeedback.processed_disjoint_newlyObservedBefore · BanditRLProof.DelayedFeedback.processed_union_newlyObservedBefore · BanditRLProof.DelayedFeedback.processAllNew · BanditRLProof.DelayedFeedback.processAllNew_eq_observedBefore · BanditRLProof.DelayedFeedback.previousObservedBefore_subset_current · BanditRLProof.DelayedFeedback.processAllNew_from_previous_eq_current · BanditRLProof.DelayedFeedback.outstandingAt_disjoint_newlyObservedBefore
Remaining: A measurable stochastic policy kernel and recursively generated action law depending only on this view. The source's simultaneous-arrival order and BSC/EAP state-transition invariants.
Evidence: BanditRLProof/DelayedFeedback/CausalView.lean; BanditRLProof/DelayedFeedback/Processing.lean; Tests/DelayedFeedbackPaperAuditCanary.lean
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.
Lean: BanditRLProof.DelayedFeedback.inactiveArms · BanditRLProof.DelayedFeedback.activeEqualShare · BanditRLProof.DelayedFeedback.delayedSAPOProbability · BanditRLProof.DelayedFeedback.delayedSAPOProbability_of_active · BanditRLProof.DelayedFeedback.delayedSAPOProbability_of_inactive · BanditRLProof.DelayedFeedback.activeEqualShare_nonneg · BanditRLProof.DelayedFeedback.delayedSAPOProbability_nonneg · BanditRLProof.DelayedFeedback.sum_delayedSAPOProbability_eq_one
Remaining: A source-faithful EAP state and proof that every update preserves nonnegative inactive mass at most one. A measurable sampling kernel using this vector on the recursively generated delayed-feedback history; the one-round probability measure is compiled downstream.
Evidence: BanditRLProof/DelayedFeedback/ActiveAllocation.lean; Tests/DelayedFeedbackPaperAuditCanary.lean
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.
Lean: BanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot · BanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.eliminated · BanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.remainingActive · BanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.mem_eliminated_iff · BanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.mem_remainingActive_iff · BanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.OptimalArmSurvivalCertificate · BanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.optimal_mem_remainingActive_of_certificate · BanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.remainingActive_nonempty_of_certificate · BanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.sum_delayedSAPOProbability_after_elimination_eq_one · BanditRLProof.DelayedFeedback.DelayedSAPOAllocation · BanditRLProof.DelayedFeedback.DelayedSAPOAllocation.probability · BanditRLProof.DelayedFeedback.DelayedSAPOAllocation.probability_nonnegative · BanditRLProof.DelayedFeedback.DelayedSAPOAllocation.sum_probability_eq_one · BanditRLProof.DelayedFeedback.DelayedSAPOAllocation.finiteActionDistribution · BanditRLProof.DelayedFeedback.DelayedSAPOAllocation.actionMeasure · BanditRLProof.DelayedFeedback.DelayedSAPOAllocation.actionMeasure_isProbabilityMeasure · BanditRLProof.DelayedFeedback.causalDelayedSAPOActionMeasureRule · BanditRLProof.DelayedFeedback.causalDelayedSAPOActionMeasureRule_isProbabilityMeasure · BanditRLProof.DelayedFeedback.causalDelayedSAPOActionMeasureRule_eq_of_observation_equivalent
Remaining: The Definition-D.1 count, phase, error, and delay clauses, their probability bound, and full recursive source Lemma D.9. EAP preservation of its inactive-probability premises. Coordinate measurability, a Markov kernel over generated histories, and recursive delayed trajectory generation.
Evidence: BanditRLProof/DelayedFeedback/Elimination.lean; BanditRLProof/DelayedFeedback/ActionLaw.lean; Tests/DelayedFeedbackPaperAuditCanary.lean; proof-obligations/PAPER-AUDIT-NEURIPS-2025-DELAYED-BOBW-FEASIBILITY.md
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.
Lean: BanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot · BanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.sourceUcbStar · BanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.EliminationGoodEvent · BanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.optimalMean_le_ucbStar_of_eliminationGoodEvent · BanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.optimalArmSurvivalCertificate_of_eliminationGoodEvent · BanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.optimal_mem_remainingActive_of_eliminationGoodEvent · BanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.eliminationGoodEventSet · BanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.optimalSurvivalEventSet · BanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.eliminationGoodEventSet_subset_optimalSurvivalEventSet · BanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.measure_optimalSurvivalEventSet_compl_le · BanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.measure_optimalSurvivalEventSet_compl_le_of_goodEvent
Remaining: The full Definition D.1 count, phase, error, and delay clauses and their measurable simultaneous event. The D.2--D.7 concentration/counting lemmas that produce the six component probability bounds. Persistence across the recursive Delayed SAPO state machine and the stochastic/adversarial regret endpoints.
Evidence: BanditRLProof/DelayedFeedback/StochasticGoodEvent.lean; Tests/DelayedFeedbackPaperAuditCanary.lean; proof-obligations/PAPER-AUDIT-NEURIPS-2025-DELAYED-BOBW-FEASIBILITY.md
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: BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventComponent · BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily · BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.componentFailure · BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.failureSet · BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.sourceGoodEventSet · BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.sourceGoodEventSet_compl · BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.measure_sourceGoodEventSet_compl_le_sum · BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.quadraticFailureBudget · BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.linearFailureBudget · BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.quadraticFailureBudget_le_linearFailureBudget · BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.measure_sourceGoodEventSet_compl_le_nine_div · BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.measure_eliminationGoodEventSet_compl_le_nine_div · BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.measure_optimalSurvivalEventSet_compl_le_nine_div
Remaining: Source-faithful random variables, events, and proofs of Lemmas D.2--D.7 on one generated Delayed SAPO law. A proved projection from the complete Definition-D.1 event to the compiled elimination slice. Recursive optimal-arm persistence and either paper-level regret endpoint.
Evidence: BanditRLProof/DelayedFeedback/StochasticGoodEventAssembly.lean; Tests/DelayedFeedbackPaperAuditCanary.lean; proof-obligations/PAPER-AUDIT-NEURIPS-2025-DELAYED-BOBW-FEASIBILITY.md
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.
Lean: BanditRLProof.UCB.integral_realKernelRegret_armStreamAction_le_lml_sum
Remaining: Direct imported-LML symbol and toolchain identity remain cross-toolchain work; the local expected pull-count ledger is already compiled. Do not treat the upstream theorem card as a local proof term.
Evidence: tasks/BRL-UCB-PORT-001.md
The stationary local endpoint is complete, but posterior-law producers outside that model and exact upstream compatibility remain separate obligations.
Remaining: Add posterior-law producers for broader models. Close the exact upstream compatibility gate.
Evidence: tasks/BRL-TS-BAYES-001.md
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.
Lean: BanditRLProof.DelayedFeedback.sourceEmpiricalWidthScale · BanditRLProof.DelayedFeedback.sourceEmpiricalWidthScale_antitone · BanditRLProof.DelayedFeedback.one_le_ten_mul_sourceEmpiricalWidthScale_of_count_le_96_mul_scale · BanditRLProof.DelayedFeedback.one_le_ten_mul_sourceEmpiricalWidthScale_two_log_of_small_count · BanditRLProof.DelayedFeedback.sourceEmpiricalWidthScale_one_one · BanditRLProof.DelayedFeedback.sourceEmpiricalWidthScale_one_four · BanditRLProof.DelayedFeedback.not_sourceEmpiricalWidthScale_one_le_four · BanditRLProof.DelayedFeedback.not_sourceEmpiricalWidthScale_horizon_four_one_le_four · BanditRLProof.DelayedFeedback.eight_mul_empiricalWidth_lt_gap_of_mem_eliminated · BanditRLProof.DelayedFeedback.gap_le_sixteen_mul_empiricalWidth_of_mem_remainingActive · BanditRLProof.DelayedFeedback.gap_le_sixteen_mul_empiricalWidth_of_mem_remainingActive_of_large_or_small_count · BanditRLProof.DelayedFeedback.gap_le_twenty_mul_gap_at_earlier_elimination_snapshot · BanditRLProof.DelayedFeedback.gap_le_twenty_mul_gap_at_earlier_elimination_snapshot_of_large_or_small_count · BanditRLProof.DelayedFeedback.DelayedSAPOD10D12GapOrderingContract · BanditRLProof.DelayedFeedback.DelayedSAPOD10D12GapOrderingContract.surrogateGap · BanditRLProof.DelayedFeedback.DelayedSAPOD10D12GapOrderingContract.surrogateGap_le_gap · BanditRLProof.DelayedFeedback.DelayedSAPOD10D12GapOrderingContract.gap_le_two_mul_surrogateGap · BanditRLProof.DelayedFeedback.DelayedSAPOD10D12GapOrderingContract.d12_gap_ordering_chain · BanditRLProof.DelayedFeedback.DelayedSAPOD10D12GapOrderingContract.gap_le_twenty_mul_gap_of_eliminationPrefixIndex_le
Remaining: A recursive Delayed SAPO processed trace that produces the actual large/small-count branch certificate, the source-width/count equality in the small branch, the current-UCB and optimal-to-later factor-three edges in the large branch, and the later-to-earlier factor-ten comparison used by the conditional same-snapshot skeleton. A source amendment or author clarification for the intended printed D.10 prefix-to-elimination width step; the compiled conditional skeleton bypasses rather than validates that step. Unconditional source Lemmas D.10/D.12, main-text Lemma 4.2, Theorem 4.1, and either regret endpoint.
Evidence: BanditRLProof/DelayedFeedback/StochasticGapOrderingAudit.lean; Tests/DelayedFeedbackPaperAuditCanary.lean; research-wiki/papers/neurips-2025-delayed-bobw-audit.md; proof-obligations/PAPER-AUDIT-NEURIPS-2025-DELAYED-BOBW-FEASIBILITY.md
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.
Lean: BanditRLProof.DelayedFeedback.SameAlgorithmMultiRegimeContract · BanditRLProof.DelayedFeedback.SameAlgorithmMultiRegimeContract.stochasticClaim · BanditRLProof.DelayedFeedback.SameAlgorithmMultiRegimeContract.adversarialClaim · BanditRLProof.DelayedFeedback.SameAlgorithmMultiRegimeContract.stochasticClaim_iff_shared_fields · BanditRLProof.DelayedFeedback.SameAlgorithmMultiRegimeContract.adversarialClaim_iff_shared_fields
Remaining: The complete Definition-D.1 event, its D.2--D.7 component probability producers, Delayed SAPO BSC/EAP state machines, switching rule, and ordered update semantics. A measurable causal randomized sampling kernel and recursively generated delayed-feedback trajectory law; only the one-round measure-valued rule now compiles. Recursive branch/count/width producers for the large/small-count conditional D.12 skeleton, the same-prefix factor-ten comparison, a clarification or amendment of the printed D.10 transport, and an unconditional D.12 / main-text Lemma 4.2 bridge. The stochastic-instance and oblivious-adversarial regret endpoints for the same algorithm identity.
Evidence: research-wiki/papers/prospective-audit-2025-freeze.json; research-wiki/papers/neurips-2025-delayed-bobw-audit.md; proof-obligations/PAPER-AUDIT-NEURIPS-2025-DELAYED-BOBW-FEASIBILITY.md
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.
Lean: No local declaration yet.
Remaining: Freeze the provider, immutable model version, replicate semantics, token/tool/build/time/cost budgets, retry and missing-run policies. Publish and freeze the final production checker image from a reviewed candidate, freeze the provider image and commands, and pass all seven bound checker probes: network denial, host-sentinel protection, operator-ground-truth absence, controller/worker output protection, patched-source/controller-input read-only enforcement, mounted-input/cidfile protection, and background-process reaping under the exact image. Pass the preregistered real-provider/real-sandbox one-case-by-three-condition smoke, excluded only from the primary analysis. Complete the frozen-model source-absent wording control and independent blind wording review; freeze hash-verified source paths, grader identities, the sealed pack digest, and blind-packet procedure. Execute and neutrally check all 450 matched runs, complete independent grading, and analyze the frozen target-level endpoints.
Evidence: evaluation/target-drift-v2/protocol.json; evaluation/target-drift-v2/paired-requirements.json; evaluation/target-drift-v2/adapter-contract.json; evaluation/target-drift-v2/checker-sandbox-contract.json; evaluation/target-drift-v2/checker-isolation-probe.template.json; evaluation/target-drift-v2/checker-image.Containerfile; evaluation/target-drift-v2/checker-image-sbom.template.json; evaluation/target-drift-v2/checker-image-candidate-32137509103.json; evaluation/target-drift-v2/execution-template.json; .github/workflows/target-drift-checker-image.yml; tools/audit_target_drift_wording.py; tools/validate_target_drift_suite_v2.py; tools/prepare_target_drift_checker_image.py; tools/target_drift_checker_cache_manifest.py; tools/finalize_target_drift_config.py; tools/run_target_drift_execution.py; tools/check_target_drift_run.py; tools/launch_target_drift_checker_container.py; tools/check_target_drift_container_controller.py; tools/check_target_drift_inner.py; tools/record_target_drift_checker_isolation_probe.py; tools/prepare_target_drift_grading.py; tools/assemble_target_drift_grades.py; tools/analyze_target_drift_execution.py
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.
Lean: No local declaration yet.
Remaining: Reconcile ABRL's Lean 4.29.1 and Mathlib v4.29.1 environment with the recorded LML seed's newer Lean/Mathlib toolchain in an isolated migration build. Add a pinned LML dependency and compile the real LeanMachineLearning.Online.Bandit.Algorithms.ETC and UCB imports. Consume the actual upstream symbols in ABRL wrapper theorems without copied or shadow declarations. Pass the complete Lean, test, license, notice, attribution, and website gates on the unified toolchain.
Evidence: lean-toolchain; lakefile.lean; research-wiki/lml/theorem-cards.md
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.
Lean: BanditRLProof.Budget.isStoppingTime_budgetExhaustionTime_of_adapted
Remaining: Resource-consumption and feasibility model. Primal-dual comparison. Final resource-constrained regret assembly.
Evidence: research-wiki/theory-tree/lean-route-roadmap.json
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.
Lean: No local declaration yet.
Remaining: A Chapter 16 one-arm event/information consumer of the compiled Lemma 15.1 history-KL decomposition. The exact per-arm information constraint and liminf extraction, with zero, finite, and infinite d_inf branches. Lemma 16.3's finite-time event/regret bridge and Theorem 16.4's exact Gaussian aggregation.
Evidence: tasks/TEXTBOOK-PART-IV-CHAPTER-16-INSTANCE-DEPENDENT-LOWER-BOUNDS-SPINE.md; proof-attempts/TEXTBOOK-PART-IV-CHAPTER-16-INSTANCE-DEPENDENT-LOWER-BOUNDS-SPINE/HistoryInformationBlocker.md
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.
Lean: No local declaration yet.
Remaining: The stochastic branch's tail-event and regret consumer of the compiled Lemma 15.1 history-KL decomposition. The exact Corollary 17.3 tail integral with its one-policy/all-horizon/all-confidence quantifiers. The correlated clipped-normal reward-matrix law, Claim 17.6 information calculation, pathwise Eq. (17.8), Claim 17.7 concentration, and Theorem 17.4 assembly.
Evidence: tasks/TEXTBOOK-PART-IV-CHAPTER-17-HIGH-PROBABILITY-LOWER-BOUNDS-SPINE.md; proof-attempts/TEXTBOOK-PART-IV-CHAPTER-17-HIGH-PROBABILITY-LOWER-BOUNDS-SPINE/ConnectedBlockers.md
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.
Lean: No local declaration yet.
Remaining: Chapter 15 regret/event bridge from the compiled same-policy history-KL identity, natural-count connection to the real-valued Delta tuning, exact 1/27 terminal, and infimum/supremum extraction.
Evidence: tasks/TEXTBOOK-PART-IV-CHAPTER-13-BASIC-LOWER-BOUND-SPINE.md; tasks/TEXTBOOK-PART-IV-CHAPTER-15-MINIMAX-LOWER-BOUNDS-SPINE.md
| Route | Priority | Registry's compiled core summary | Next registered leaves |
|---|---|---|---|
ROUTE-ETC-FINITE-STOCHASTICExplore-Then-Commit finite stochastic regret |
active | ETC round-robin counts · fixed-commit trace phase boundary · empirical mean measurability · argmax oracle · wrong-commit event reduction · bounded reward source contracts · infinitePi wrong-commit bound · ENNReal.ofReal lower-integral regret assembly | convert lower-integral ETC surrogate to the desired Bochner/Rat expected-regret theorem · generalize fixed actionWithCommit source to policy-generated adaptive traces · extract reusable bounded-centered reward sub-Gaussian contracts into Mathlib-shaped statements |
ROUTE-UCB1-FINITE-STOCHASTICUCB1 logarithmic finite-arm regret |
active-next | pull-count regret decomposition · expected pull-count decomposition · finite-horizon bad-event union/summability · sub-Gaussian tail wrappers | define non-placeholder UCB score with sqrt/log confidence width · prove positive count after initialization · prove UCB maximality implies suboptimal pull has a bad event or small count · prove confidence-width algebra and logarithmic count bound · assemble expected pull count and regret |
ROUTE-KL-UCBKL-UCB bounded stochastic bandits |
planned | finite arms and regret decomposition · tail union wrappers | Bernoulli KL definition and nonnegativity · KL monotonicity/inversion for confidence sets · bounded reward KL confidence route · KL-UCB index maximality and pull-count bound |
ROUTE-THOMPSON-BAYESThompson sampling and Bayesian regret |
planned | posterior kernel surface · posterior action identity ledger · finite/countable best-action measurability · conditional expectation bridge · expected regret decomposition | Bayes prior/environment product law · posterior action-law construction or LML import · noncountable posterior best-action measurability if needed · Bayesian regret integrability contract · clipped-UCB or information-ratio bridge |
ROUTE-EXP3-ADVERSARIALEXP3 adversarial finite-arm regret |
planned | finite exponential-weights potential · updated-potential unfolding · potential telescoping | probability simplex sampling API · importance-weighted estimator unbiasedness · exp x <= 1 + x + x^2 route under bounded losses · learning-rate optimization |
ROUTE-TSALLIS-INF-FTRLTsallis-INF and finite-arm FTRL best-of-both-worlds |
planned | FTRL one-step inequality under explicit minimizer certificate · finite-simplex predicate · Tsallis power sum and negative entropy well-definedness | finite-simplex convexity and feasible minimizer existence · Tsallis regularizer convexity and derivative/subgradient shape · stability/penalty decomposition · self-bounding conversion · adaptive learning-rate schedule algebra |
ROUTE-BOBW-LINEAR-CONTEXTUALBest-of-both-worlds linear contextual bandits |
watchlist | FTRL/Tsallis finite-action surface · policy measurability surface · finite regret decomposition | context distribution and margin condition contract · linear loss estimator · covariance/Gram matrix inverse or inverse-free route · BoBW stochastic/adversarial split |
ROUTE-LINEAR-OFULOFUL and LinUCB linear bandit regret |
planned | policy measurability surface · martingale-difference prefix contracts · finite regret decomposition | finite-dimensional feature vector API · Gram matrix PSD and monotonicity · least-squares estimator and confidence ellipsoid · elliptical potential lemma · self-normalized concentration theorem card/import route |
ROUTE-CONTEXTUAL-EXP4-LINUCBcontextual bandits: EXP4, LinUCB, and policy regret |
planned | policy measurability · reward kernel surface · finite trajectory kernels | context/history API · policy class regret definition · expert advice mixture over policies · offline evaluation/IPW regularity contracts |
ROUTE-RL-UCBVIfinite-horizon RL and UCB-VI regret |
compiled-canonical | reward kernel surface · policy-generated traces · finite trajectory kernel ingredients · martingale-difference contracts · finite MDP data and measurable one-step Bellman action-value surface · stage-indexed Markov policy evaluation with induced state kernels and Bellman recursion · generated finite policy trajectory and expected cumulative-reward value identity · finite-action Bellman optimality and measurable greedy-policy attainment · true state occupancy and exact expected-regret performance difference · optimistic Bellman certificate and true-occupancy bonus regret bound · estimated reward/transition confidence transport, estimated-greedy policy, and factor-two selected-radius single-episode regret bound · finite-state singleton transition-coordinate errors and recursive-tail envelopes transported into Bellman confidence and the optimistic-regret endpoint · stochastic sampled cumulative return around recursive policy value with exact reward-noise/Bellman split, additive conditional MGF proxy, and fixed-horizon two-sided tail · same-prefix aggregate generated transition numerators and visit denominators with exact row-sum and successor alignment · previous-Q clipped recurrent known-reward UCBVI-CH planner with optimistic zero count and measurable finite argmax · joint singleton-Bernstein and normalized optimal-tail confidence on the recurrent source trajectory measure · all-episode recurrent Bellman optimism and generated raw episode pseudo-regret decomposition · actual-count charge summation and generated-filtration Bellman innovation tail · frozen 20/250 high-probability UCBVI-CH terminal and integrable expectation bound plus K H delta | Bernstein or variance-aware empirical transition confidence and total-variance summation for the separate minimax milestone · stochastic-reward UCBVI confidence and changed terminal constants · realized sampled-return high-probability regret on the canonical recurrent source · posterior-sampling, model-free, or continuous-space RL extensions |
ROUTE-BWK-RESOURCEbandits with knapsacks and resource constraints |
planned | budget stopping-time wrapper · finite pull-count/regret decomposition | resource consumption trace and measurability · budget feasibility invariant · primal-dual Lagrangian comparison · optional-stopping or stopped-process expectation bridge |
ROUTE-PREFERENCE-DUELINGdueling and preference bandits |
watchlist | finite actions and finite sums | pairwise preference matrix · Condorcet/Borda winner definitions · comparison feedback kernel · comparison regret decomposition |
ROUTE-ROBUST-NONSTATIONARY-DELAYEDrobust, corrupted, nonstationary, delayed, and batched bandits |
watchlist | variance concentration wrappers · finite sums and time windows · martingale/filtration surfaces · global-law oracle-restart local expected stability transport and coarse epoch certificate | windowed pull-count and reward sums · restart-local refined finite-sum and local-rate/penalty tuning under the global generated oracle-restart law, plus a law-derived schedule-epoch-cardinality bound · median-of-means/trimmed estimator contracts · delay queue and pending-feedback filtration |
ROUTE-LLM-FEDERATED-NEURALLLM, neural, recommender, and federated bandits |
watchlist | contextual policy measurability · posterior kernel surface · finite-action regret decomposition | embedding/context contract without overformalizing neural nets · model-selection action space · client-indexed trace and communication round counts · offline-to-online prior and logged-data positivity |