Teaching chapter 10 of 10 · Canonical route planned

10. Automation, resources, and open routes

The proof harness, task vocabulary, resource stopping leaves, literature registry, partial source-frozen delayed-feedback, succinct-lower-bound, and stochastic-gradient-bandit audits, and planned BwK, preference, robust, federated, neural-bandit, and sharp KL-asymptotic work.

How to read the status. It describes this page's canonical local Lean route, not completion of the cited textbook chapter or every extension listed below.

Orientation

Who should read this. Read this chapter to contribute a new route or understand what is deliberately not claimed.

Learning goals

Use the same status vocabulary for source declarations, theorem cards, tasks, and blockers.
Distinguish a stopping-time foundation from a completed resource-constrained algorithm theorem.
Move a literature target through task packets, proof obligations, compilation, and synchronized documentation.

Textbook crosswalk

Read the mathematics before the Lean interface

The Book Map is a curated formalization curriculum anchored in Bandit Algorithms, not a chapter-for-chapter reproduction of one book. Visible page labels use the numbered pages of its free online edition; source buttons use the PDF viewer's physical page index, which includes front matter and can therefore be larger. Companion papers cover algorithm-specific results.

Primary spine · free online edition

Bandit Algorithms

Tor Lattimore and Csaba Szepesvári

Location: Parts VII–VIII as a background index
Pages: online pp. 358–538

Open at the cited pages

Algorithm-specific companion

A Novel General Framework for Sharp Lower Bounds in Succinct Stochastic Bandits

Guo Zeng and Jean Honorio

Location: Section 3.1; Theorem 3.8 context in Section 3.2
Pages: physical PDF pp. 4–5 and 11–12

Open at the cited pages

Algorithm-specific companion

Does Stochastic Gradient really succeed for Bandits?

Dorian Baudry, Emmeran Johnson, Simon Vary, Ciara Pike-Burke, and Patrick Rebeschini

Location: Section 1.2, Algorithm 1, Theorem 1, Corollary 1, Theorem 2, Equations (3)–(11), Appendix A.1, Appendix C, Theorem 4, and Appendix E Steps 1–4
Pages: physical PDF pp. 2–6, 22, 31–40, and 47–49

Open at the cited pages

source algorithm · ordered flow

Stochastic Gradient Bandit (Algorithm 1)

Read top to bottom: each step supplies the state or proof fact used by the next one.

Initialize θ
Set θₖ,₁ = 0; the initial action law is uniform.
Softmax law
Set pₖ,ₜ proportional to exp(θₖ,ₜ) over the finite arms.
Sample reward
Draw Aₜ from pₜ and observe the selected arm's reward rₜ.
Update θ
Add η rₜ(1{Aₜ = k} − pₖ,ₜ) to every coordinate.
Split regret
Expected gap increments plus failure mass yield the finite-horizon bound.

Algorithm · explicit conventions

Source Algorithm 1: stochastic-gradient bandit

The source-frozen loop makes the zero initialization, softmax action law, selected reward, and simultaneous coordinate update explicit.

Softmax probability and parameter update. Formula renderer unavailable; readable fallback: Sample from the softmax of theta, observe the selected reward, and add eta times reward times selected-indicator minus probability to every arm coordinate.\[p_{k,t}=\frac{e^{\theta_{k,t}}}{\sum_j e^{\theta_{j,t}}},\qquad \theta_{k,t+1}=\theta_{k,t}+\eta r_t\left(\mathbf 1\{A_t=k\}-p_{k,t}\right).\]

input: K arms, constant learning rate η, horizon T; set θ_{k,1} = 0
for t = 1,…,T:
    compute p_{k,t} = exp(θ_{k,t}) / sum_j exp(θ_{j,t})
    sample A_t from p_t and observe reward r_t from the selected arm
    for every k: θ_{k,t+1} = θ_{k,t} + η r_t (1{A_t=k} - p_{k,t})

Source/Lean boundary. BanditRLlib compiles the source Theorem-1 endpoint for its bounded two-arm fixed-IID trajectory and a direct Corollary-1 consumer. Theorem 2's phase trigger/no-return/ballot assembly and Theorems 3–4 remain open; this pseudocode does not promote those terminals.

Worked example · follow one decision

Follow one theorem route without promoting an open terminal

The SGB Theorem-2 audit is a useful example of how the Frontier page separates a paper target, compiled infrastructure, and the first genuinely missing mathematical bridge.

Freeze the source target
The theorem concerns the supercritical two-arm regime and a polynomial regret lower bound, so a finite-horizon helper cannot replace the endpoint.
Worked example step 1. Formula renderer unavailable; readable fallback: Above the critical learning rate, the source target is a polynomial regret lower bound up to logarithmic factors.\[\eta>\lambda_\Delta\quad\Longrightarrow\quad R_T^{\mathrm{SGB}}=\widetilde\Omega\!\left(T^{1-(1+\varepsilon)\lambda_\Delta/\eta}\right).\]
Keep the compiled bridge at its real scope
Current Lean layers can transport a missing-pull phase into a terminal low-count event and charge any mass that already exists against finite-horizon expected pseudo-regret.
Worked example step 2. Formula renderer unavailable; readable fallback: A missing-pull event implies a low terminal optimal-arm count, and any probability mass of that event yields a finite-horizon regret charge.\[E_{\mathrm{missing}}\subseteq\{N_{a^\star}(T)<m\},\qquad \Delta(T-m)\Pr(E_{\mathrm{missing}})\le\mathbb E[\bar R_T].\]
Name what is still absent
The current route does not prove that the missing branch has positive mass, nor the all-present fixed-cutoff trigger, future no-return law, ballot probability, or asymptotic assembly.
Worked example step 3. Formula renderer unavailable; readable fallback: Positive missing-event probability is not proved by the current compiled route.\[\Pr(E_{\mathrm{missing}})>0\quad\text{is not a compiled consequence of the current route.}\]

Takeaway. A growing proof graph is scientific progress only when it closes a named interface without changing the target. Here the graph has advanced, but the source Theorem-2 terminal remains blocked.

Scope. The middle inequality is a teaching-level summary of the compiled finite-horizon charge and omits its exact indexing and nonnegativity hypotheses. Use the linked Lean declarations and source-contract cards for the authoritative statement.

5 distinct theory routes, one frontier.Open the source theorem you want to compare; the other routes stay compact.

Source routeDefinitions 3.1–3.3 and Lemmas 3.1–3.4 (succinct-support geometry)Partial source portphysical PDF pp. 4–5

Source theorem · faithful restatement

Definitions 3.1–3.3 and Lemmas 3.1–3.4 (succinct-support geometry)

Original at physical PDF pp. 4–5 ↗

Partial source port54 local declarations compile, but the global source theorem and regret endpoints do not.

The source defines its atom set, succinct-support correlation contract, Q/R pair, and finite succinct representations. Its first four lemmas identify the coefficient norms and prove strict representation-size minimality and uniqueness for a fixed vector.

Model: A finite atom system and vectors admitting the source's succinct or strictly succinct finite representations.
Assumptions: The representation, correlation, normalization, and strict-separation conditions in Definitions 3.1–3.3 hold for the compared vector.
Algorithm parameters: Atoms E_i, coefficients a_i, succinct size s, and strict succinct size z.
Regret notion: Not a regret terminal; this is the geometric support layer used by the later lower-bound argument.
Guarantee: Q and R reduce to coefficient max and l1 norms on the stated support, and strict representation size satisfies z ≤ s.

Source mathematical statement. Formula renderer unavailable; readable fallback: On a succinct support, Q is the largest absolute coefficient and R is the sum of the absolute coefficients. For the same vector, a strict succinct representation uses no more atoms than any succinct representation.\(Q(\sum_i a_i E_i)=\max_i |a_i|,\qquad R(\sum_i a_i E_i)=\sum_i |a_i|,\qquad X\text{ s-succinct and strictly z-succinct}\Rightarrow z\le s.\)

BanditRLlib relationship. BanditRLlib compiles 54 declarations for Definitions 3.1–3.3 and Lemmas 3.1–3.4, including a finite-Bessel proof of strict representation-size minimality for the same vector, and separately diagnoses a global R boundedness obligation. The global Lemmas 3.5–3.6, Assumption 3.7, Theorem 3.8, and every regret endpoint remain outside the compiled slice.

The mathematical content is restated in this site's notation; wording is ours. See physical PDF pp. 4–5 in the linked source for the original statement and full assumptions.

Source routeTheorem 1 (two-arm SGB regret upper bound)Compiled local terminalphysical PDF pp. 3–4

Source theorem · faithful restatement

Theorem 1 (two-arm SGB regret upper bound)

Original at physical PDF pp. 3–4 ↗

Compiled local terminalThe exact bounded two-arm fixed-IID theorem endpoint compiles under its recorded contract.

The source theorem combines a forward-potential logarithmic bound with a telescoping control of squared failure probability for the same fixed-IID two-arm SGB trajectory.

Model: The source's zero-initialized, constant-learning-rate stochastic-gradient bandit on a bounded fixed-IID two-arm instance.
Assumptions: The gap satisfies 0 < Δ < 1, η > 0, and ηC_η < Δ; the two reward laws have the source's fixed means and bounded support.
Algorithm parameters: Horizon T, gap Δ, learning rate η, and the analytic constant C_η.
Regret notion: Expected pseudo-regret of the actual sampled SGB actions.
Guarantee: The explicit logarithmic term plus finite failure-regret term displayed above.

Source mathematical statement. Formula renderer unavailable; readable fallback: For a two-arm bounded-reward instance, Theorem 1 gives an explicit logarithmic-in-horizon regret term plus a finite failure-regret term whenever the learning rate satisfies η Cη < Δ.\(R_T^{\mathrm{SGB}}\le \frac{\log(1+4\eta\Delta T)}{2\eta}+\frac{\Delta}{2\eta(\Delta-\eta C_\eta)},\qquad C_\eta=2\sum_{n=0}^{\infty}\frac{(2\eta)^n}{(n+2)!}\le e^{2\eta},\quad \eta C_\eta<\Delta.\)

BanditRLlib relationship. BanditRLlib compiles this exact Theorem-1 endpoint for the actual sampled pseudo-regret of bounded two-arm fixed-IID laws, specialized through a Unit Dirac environment prior. A separate eight-declaration Appendix-E gate checks finite scalar contracts used in Theorem 4, but does not prove that theorem. The Theorem-1 contract keeps 0 < Delta < 1, eta > 0, eta C_eta < Delta, exact arm means, and T = tailHorizon + 1 explicit. A later 23-declaration Corollary-1 companion compiles as a direct consumer; it is not evidence for Theorem 2.

The mathematical content is restated in this site's notation; wording is ours. See physical PDF pp. 3–4 in the linked source for the original statement and full assumptions.

Source routeCorollary 1 (horizon-indexed two-arm SGB rate)Compiled local terminalphysical PDF p. 5

Source theorem · faithful restatement

Corollary 1 (horizon-indexed two-arm SGB rate)

Original at physical PDF p. 5 ↗

Compiled local terminalA direct horizon-indexed consumer of the compiled Theorem-1 route compiles.

Corollary 1 balances the already proved small-learning-rate Theorem-1 branch against the pathwise Delta-times-T bound. It describes a horizon-indexed family of fixed-rate policies, not one policy whose rate changes during a run.

Model: The same bounded fixed-IID two-arm SGB family as Theorem 1, indexed by the target horizon.
Assumptions: Use the Theorem-1 instance assumptions and choose one constant learning rate η_T for each horizon T.
Algorithm parameters: Horizon T and η_T = √(log T/T).
Regret notion: Expected sampled-action pseudo-regret for the horizon-indexed policy family.
Guarantee: Regret is O(√(T log T)); this is not one anytime policy with a changing within-run rate.

Source mathematical statement. Formula renderer unavailable; readable fallback: For every source horizon T, choose one fixed learning rate equal to the square root of log T divided by T; the resulting two-arm regret is at most a constant times the square root of T log T.\(\eta_T=\sqrt{\log T/T}\quad\Longrightarrow\quad R_T^{\mathrm{SGB}}=O(\sqrt{T\log T}).\)

BanditRLlib relationship. Twenty-three new declarations compile an explicit finite companion on the generated zero-initialized two-arm fixed-IID trajectory with a Unit Dirac environment prior. For T >= 2 and 0 < Delta < 1, twoArmFixedIIDDirac_corollaryOne bounds expected sampled pseudo-regret by (2 + 1/log 2 + 2 exp 2) sqrt(T log T). The arm reward laws remain bounded fixed-IID laws; the Dirac measure is the prior on the singleton environment, not a claim that rewards are Dirac or Rademacher. This is a direct Theorem-1 consumer and is not independent Theorem-2 evidence.

The mathematical content is restated in this site's notation; wording is ours. See physical PDF p. 5 in the linked source for the original statement and full assumptions.

Source routeTheorem 2 (two-arm SGB phase transition)Terminal blockedphysical PDF p. 6; Appendix C pp. 31–40

Source theorem · faithful restatement

Theorem 2 (two-arm SGB phase transition)

Original at physical PDF p. 6; Appendix C pp. 31–40 ↗

Terminal blockedCompiled prerequisite layers exist; the fixed-cutoff trigger, no-return law, ballot assembly, and theorem endpoint remain open.

Appendix C reindexes the generated process by optimal-arm pull count, constructs a low-probability phase for that arm, and turns a no-return event into a long starvation interval and polynomial regret.

Model: The source's zero-initialized constant-rate SGB on its specified fixed-IID two-arm phase-transition instance.
Assumptions: The gap satisfies 0 < Δ < 1, η exceeds λ_Δ, and ε is any positive slack in the asymptotic exponent.
Algorithm parameters: Horizon T, gap Δ, rate η, threshold λ_Δ, and ε > 0.
Regret notion: Expected pseudo-regret of the sampled SGB trajectory.
Guarantee: A polynomial lower bound up to logarithmic factors with exponent 1-(1+ε)λ_Δ/η.

Source mathematical statement. Formula renderer unavailable; readable fallback: Above the two-arm critical learning rate, Theorem 2 gives a polynomial-in-horizon regret lower bound up to logarithmic factors, with the exponent reduced by an arbitrary positive epsilon.\(\lambda_\Delta=\tfrac12\log\!\frac{1+\Delta}{1-\Delta},\quad \eta>\lambda_\Delta\quad\Longrightarrow\quad R_T^{\mathrm{SGB}}=\widetilde{\Omega}\!\left(T^{1-(1+\varepsilon)\lambda_\Delta/\eta}\right)\ \text{for every }\varepsilon>0.\)

BanditRLlib relationship. The exact K = 2 target remains blocked. Twenty-five declarations compile deterministic source-shaped fixed-cutoff and terminal-count consumers, including a generic finite-horizon low-count regret charge; separate compiled layers provide chronological nth-pull semantics, latent fixed-arm products and readout, deferred-decisions prefix factorization, action/readout interfaces, count-capped branch locality, and exact deterministic-time next-reward freshness. A ten-declaration module identifies every inclusive finite prefix and proves equality of the complete visible/native trajectory measures. The selected-block module has eight declarations for missing-pull-aware block transport, fourteen for the exact finite Appendix-C `S0/S1` event, ten for an exact disjoint probability split between the generated all-present phase and an explicit missing-pull phase, and four that send the missing branch into a measurable terminal-count-below event, transport its mass to the generated trajectory, and charge that existing mass against finite-horizon expected sampled pseudo-regret. This is not a product or selected-IID theorem and supplies no positive missing-branch probability. Pull-ordered or stopped selected-reward IID remains uncompiled. The next unique leaf is the generated all-present Appendix-C phase trigger at a fixed chronological cutoff; the stopped-prefix future-cylinder law needed to prove conditional no-return probability at least one half, Rademacher/binomial ballot probability, asymptotic assembly, and the frozen Theorem-2 terminal remain uncompiled.

The mathematical content is restated in this site's notation; wording is ours. See physical PDF p. 6; Appendix C pp. 31–40 in the linked source for the original statement and full assumptions.

Source routeTheorem 4 / Appendix E source-contract windowTerminal blockedphysical PDF pp. 47–49

Source theorem · faithful restatement

Theorem 4 / Appendix E source-contract window

Original at physical PDF pp. 47–49 ↗

Terminal blockedA finite contract gate compiles, but the generated general-K process and Theorem-4 endpoint remain open.

This is the finite contract consumed by the Appendix-E transient-phase argument, not the statement of Theorem 4 itself.

Model: Finite buffer and survival events inside the source's general-K Appendix-E transient-phase route.
Assumptions: The displayed positive drift, buffer-mass, survival, and event-inclusion inequalities hold with 0 < p' and c < 1/2.
Algorithm parameters: Arm count K, gap Δ, learning rate η, C_η, buffer mass p', and loss fraction c.
Regret notion: Not the Theorem-4 regret terminal; this is a finite event-probability contract used by that proof.
Guarantee: The survival event has positive mass at least p'(1-2c).

Source mathematical statement. Formula renderer unavailable; readable fallback: The printed tuning yields a positive drift margin. For positive p-prime and c below one half, explicit buffer and conditional-survival premises make the finite survival mass at least the positive quantity p-prime times one minus two c.\[\begin{gathered}\eta C_\eta < \frac{2\Delta}{K+2},\\ 2\Delta-\eta C_\eta(K+2)>0,\\ 0<p',\quad c<\tfrac12,\\ P(B)\ge p',\\ P(B\cap S)\ge(1-2c)P(B),\\ P(B\cap S)\le P(S),\\ \Longrightarrow P(S)\ge p'(1-2c)>0.\end{gathered}\]

BanditRLlib relationship. Eight Lean declarations compile the positive margin, audited finite event composition, and finite geometric phase envelope. They expose an unresolved Step-4 conditioning/direction mismatch while leaving the general-K generated process, uniform buffer/survival producer, stopped supermartingale/Doob route, and Theorem 4 uncompiled.

The mathematical content is restated in this site's notation; wording is ours. See physical PDF pp. 47–49 in the linked source for the original statement and full assumptions.

Natural-language and Lean side by side

The mathematical readings are explanatory summaries. The exact generated Lean statement and its source link remain authoritative for hypotheses, types, constants, and indexing.

A curated route through definitions, key bridges, and canonical terminals stays visible. 25 additional dependency, extension, or research-frontier notes are grouped below.

Mathematics ↔ Lean

A typed contract for every harness task

Lean declarationBanditRLProof.HarnessTask

Compiled

Plain-English statement. A harness task records the target, task kind, status, source and scenario cards, profile, required artifacts, and acceptance gates used by the automation system.

Mathematical reading. Formula renderer unavailable; readable fallback: A harness task records the target, task kind, status, source and scenario cards, profile, required artifacts, and acceptance gates used by the automation system.\(\text{task}=\text{target}+\text{evidence}+\text{status}+\text{artifacts}+\text{gates}.\)

Intuition: Proof automation is safer when completion criteria are data that can be inspected, rather than an informal instruction that can drift across runs.
Why it is needed: The website uses the same status discipline: a theorem card, a planned target, and a compiled Lean theorem are visibly different objects.
Place in the proof: This structure belongs to the automation layer rather than the mathematical bandit theory.

Proof and Lean reading notes

Proof idea: It is a structure definition. The default Lean gate later instantiates the acceptance condition with the repository's build command.
Lean reading notes: Inductive TaskStatus and TaskKind values make invalid status strings unrepresentable inside Lean-side harness data.
Teaching dependencies: No direct teaching dependency recorded.

Exact Lean statement

structure HarnessTask where

Open in the declaration catalog Open source at line 53

Mathematics ↔ Lean

Strict succinct representations use no more atoms

Lean declarationBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.succinctSize_ge_strictSize

Compiled

Plain-English statement. If one representation of X uses s succinct atoms and another is strictly z-succinct, then z is at most s.

Mathematical reading. Formula renderer unavailable; readable fallback: If one representation of X uses s succinct atoms and another is strictly z-succinct, then z is at most s.\(X\text{ is }s\text{-succinct and strictly }z\text{-succinct}\Longrightarrow z\le s.\)

Intuition: Strict nonzero coefficients prevent any direction in the second support from being hidden. Equality of the local R values forces unit correlations with one signed support combination, and finite Bessel bounds how many orthonormal strict-support atoms can all attain correlation one.
Why it is needed: This is the compiled source-shaped content of Zeng–Honorio Lemma 3.3. Together with its two-direction consumer for Lemma 3.4, it makes strict succinct representation size intrinsic.
Place in the proof: Definitions 3.1–3.3 and Lemmas 3.1–3.4 now compile. The result does not repair the paper's globally real-valued R interface or prove Lemmas 3.5–3.6, Assumption 3.7, Theorem 3.8, or a regret bound.

Proof and Lean reading notes

Proof idea: Build the signed support combination for the first representation, identify its squared norm with s, show every strict-support basis vector has absolute inner product one, and apply the finite Bessel inequality to obtain z <= s.
Lean reading notes: The proof uses Mathlib's finite Orthonormal.sum_inner_products_le. It needs neither a spanning assumption nor an ambient dimension bound because the argument is confined to two finite representations.
Teaching dependencies: BanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.SuccinctRepresentation.sumAbs_eq, BanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.SuccinctRepresentation.abs_inner_strictBasis_supportSignCombination_eq_one, BanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.orthonormal, BanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.SuccinctRepresentation.norm_sq_supportSignCombination_eq_size

Exact Lean statement

theorem succinctSize_ge_strictSize {system : SuccinctUnitSystem V} {x : V} {s z : Nat} (hs : IsSuccinctAt system x s) (hz : IsStrictlySuccinctAt system x z) : z ≤ s

Open in the declaration catalog Open source at line 640

Mathematics ↔ Lean

Source-faithful two-arm SGB Theorem 1

Lean declarationBanditRLProof.StochasticGradientBandit.twoArmFixedIIDDirac_theoremOne

Compiled

Plain-English statement. For the source's bounded two-arm fixed-IID SGB process, the expected pseudo-regret of the actual sampled actions satisfies the exact Theorem-1 logarithmic term plus its finite failure-regret term.

Mathematical reading. Formula renderer unavailable; readable fallback: For the source's bounded two-arm fixed-IID SGB process, the expected pseudo-regret of the actual sampled actions satisfies the exact Theorem-1 logarithmic term plus its finite failure-regret term.\(R_T^{\mathrm{SGB}}\le \frac{\log(1+4\eta\Delta T)}{2\eta}+\frac{\Delta}{2\eta(\Delta-\eta C_\eta)}.\)

Intuition: The generated Equation-(5) drift turns cumulative regret into one expected best-coordinate parameter plus squared failure probability. The forward exponential potential controls the parameter through Jensen and log, while the inverse potential telescopes the failure squares.
Why it is needed: This is a dependency-closed external-paper endpoint rather than a theorem-shaped algebraic leaf: it joins the generated policy, reward laws, actual sampled actions, trajectory measure, expectation, horizon convention, and source constants.
Place in the proof: This compiles Baudry et al. Theorem 1 only for two bounded fixed-IID arm laws with a Dirac environment prior. Theorems 2–4, general-K rates, and non-Dirac environment mixtures remain outside this endpoint.

Proof and Lean reading notes

Proof idea: Prove the conditional Equation-(5) source increment on the generated history, telescope its expectation into the best parameter, decompose failure mass into success-failure plus its square, bound the forward potential and apply Jensen/log, telescope the inverse potential, identify actual sampled-action regret with generated expected regret, and specialize the environment to fixed IID laws under a Dirac prior.
Lean reading notes: The assumptions retain eta > 0, 0 < Delta < 1, eta C_eta < Delta, rewards supported in [-1,1], exact arm means with mean(0)-mean(1)=Delta, and T = tailHorizon + 1. Lean arm 0 is the source's optimal arm 1; no online compilation service or unverified broader theorem is implied.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.integral_twoArmSampledPseudoRegret_le_sourceTheoremOne, BanditRLProof.StochasticGradientBandit.integral_twoArmSampledPseudoRegret_eq_generated, BanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironment_contract

Exact Lean statement

theorem twoArmFixedIIDDirac_theoremOne (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (mean : Fin 2 -> Real) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, |reward| <= 1) (hmean : forall arm, integral (armLaw arm) id = mean arm) (eta Delta : Real) (heta : 0 < eta) (hDelta : 0 < Delta) (_hDelta_lt_one : Delta < 1) (hgap : mean 0 - mean 1 = Delta) (hmargin : eta * sourceC eta < Delta) (tailHorizon : Nat) : integral (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) (twoArmSampledPseudoRegret (Env := Unit) Delta (tailHorizon + 1)) <= Real.log (1 + 4 * eta * Delta * ((tailHorizon + 1 : Nat) : Real)) / (2 * eta) + Delta / (2 * eta * (Delta - eta * sourceC eta))

Open in the declaration catalog Open source at line 1131

Mathematics ↔ Lean

Positive survival mass in the Theorem 4 contract

Lean declarationBanditRLProof.StochasticGradientBandit.theoremFourStepFour_survivalMass_pos

Compiled

Plain-English statement. For positive p-prime and c below one half, a buffered event with mass at least p-prime and conditional joint-survival mass at least one minus twice c yields strictly positive unconditional survival mass.

Mathematical reading. Formula renderer unavailable; readable fallback: For positive p-prime and c below one half, a buffered event with mass at least p-prime and conditional joint-survival mass at least one minus twice c yields strictly positive unconditional survival mass.\[0<p',\;c<\tfrac12,\;P(B)\ge p',\;P(B\cap S)\ge(1-2c)P(B),\;P(B\cap S)\le P(S)\;\Longrightarrow\;P(S)\ge p'(1-2c)>0.\]

Intuition: The finite argument is ordinary total-probability bookkeeping: first enter a strict buffer with positive mass, then retain a positive fraction of that mass on the survival event.
Why it is needed: Appendix E Step 3 needs a uniform positive return-avoidance probability. Isolating the exact finite consumer keeps the unresolved event-conditioning and bound-direction mismatch visible before the later stopped-process proof.
Place in the proof: This is an Appendix-E source-contract audit leaf, not Theorem 4. The general-K generated SGB process, uniform buffered-event producer, stopped supermartingale/Doob route, and final regret bound remain open.

Proof and Lean reading notes

Proof idea: Multiply the buffer lower bound by the nonnegative factor one minus twice c, compose with the joint-survival premise, and use event inclusion into survival mass.
Lean reading notes: All quantities are finite real masses supplied explicitly. The declaration constructs no probability space, conditional probability, stopping time, or generated bandit trajectory.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.theoremFourStepFourSurvivalLowerBound_pos, BanditRLProof.StochasticGradientBandit.theoremFourStepFour_survivalMass_ge

Exact Lean statement

theorem theoremFourStepFour_survivalMass_pos (pPrime c bufferedMass jointSurvivalMass survivalMass : Real) (hpPrime : 0 < pPrime) (hc_half : c < 1 / 2) (hbuffer : pPrime <= bufferedMass) (hconditional : (1 - 2 * c) * bufferedMass <= jointSurvivalMass) (hsubset : jointSurvivalMass <= survivalMass) : 0 < survivalMass

Open in the declaration catalog Open source at line 93

Explore 25 additional Lean teaching notes

Mathematics ↔ Lean

The first time an adapted cumulative spending process reaches a fixed…

Lean declarationBanditRLProof.Budget.isStoppingTime_budgetExhaustionTime_of_adapted

Compiled

Plain-English statement. The first time an adapted cumulative spending process reaches a fixed budget is a stopping time.

Mathematical reading. Formula renderer unavailable; readable fallback: The first time an adapted cumulative spending process reaches a fixed budget is a stopping time.\(\tau_B=\inf\{t:\mathrm{spent}_t\ge B\}\quad\Longrightarrow\quad\{\tau_B\le n\}\in\mathcal F_n.\)

Intuition: Whether the budget has been exhausted by time n can be decided from information available by time n.
Why it is needed: Any rigorous bandits-with-knapsacks route must stop at a random, history-observable exhaustion time.
Place in the proof: This is a compiled foundation leaf, not a BwK model or regret theorem.

Proof and Lean reading notes

Proof idea: Express exhaustion as Mathlib's hittingAfter construction and use adaptedness to prove measurability of each level event.
Lean reading notes: The stopping time takes values in WithTop Nat, allowing the budget never to be reached.
Teaching dependencies: No direct teaching dependency recorded.

Exact Lean statement

theorem isStoppingTime_budgetExhaustionTime_of_adapted {Omega : Type u} [mOmega : MeasurableSpace Omega] {F : Filtration Nat mOmega} {spent : Nat -> Omega -> Nat} (budget : Nat) (hspent : Adapted F spent) : IsStoppingTime F (budgetExhaustionTime spent budget)

Open in the declaration catalog Open source at line 36

Mathematics ↔ Lean

On a succinct support, the paper's Q quantity of a finite support…

Lean declarationBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.sourceQ_supportCombination_eq

Compiled

Plain-English statement. On a succinct support, the paper's Q quantity of a finite support combination is exactly the largest absolute coefficient.

Mathematical reading. Formula renderer unavailable; readable fallback: On a succinct support, the paper's Q quantity of a finite support combination is exactly the largest absolute coefficient.\(Q(\sum_i a_i E_i)=\max_i |a_i|\).

Intuition: The support contract makes the chosen support atoms orthogonal. Every atom in the source atom set correlates with the combination by at most the largest coefficient, while a signed maximizing support atom reaches that value.
Why it is needed: This is Zeng–Honorio Lemma 3.1 and the reusable coefficient geometry needed before the paper's information–regret construction.
Place in the proof: The identity is compiled. It does not imply that Q separates all ambient vectors or that the globally defined real-valued R is finite everywhere.

Proof and Lean reading notes

Proof idea: Use the support correlation-sum bound for the upper inequality, derive mutual orthogonality, choose an index attaining the finite maximum, and use the positive or negative maximizing atom as the lower-bound witness.
Lean reading notes: The atom set remains an arbitrary Set, the support size is finite and nonempty, and the literal real sSup contract is retained. A separate compiled diagnostic shows why global R needs additional regularity outside the succinct span.
Teaching dependencies: BanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.correlationSum_le_one, BanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.inner_basis_basis, BanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.exists_abs_eq_maxAbsCoefficient

Exact Lean statement

theorem sourceQ_supportCombination_eq [Nonempty (Fin s)] (support : IsSuccinctSupport system basis) (a : Fin s → ℝ) : system.sourceQ (supportCombination basis a) = maxAbsCoefficient a

Open in the declaration catalog Open source at line 292

Mathematics ↔ Lean

After fixing the pre-action history, the expected SGB update of coordinate…

Lean declarationBanditRLProof.StochasticGradientBandit.expectedSourceIncrement_eq_gapCoordinate

Compiled

Plain-English statement. After fixing the pre-action history, the expected SGB update of coordinate k is its sampling probability times instantaneous expected gap minus that arm's gap.

Mathematical reading. Formula renderer unavailable; readable fallback: After fixing the pre-action history, the expected SGB update of coordinate k is its sampling probability times instantaneous expected gap minus that arm's gap.\(\mathbb E_t[\delta\theta_{k,t}]=p_{k,t}(\mathbb E_t[\Delta_{A_t}]-\Delta_k).\)

Intuition: A coordinate grows only when its arm's gap is smaller than the policy's current average gap. The softmax probability scales how strongly that comparison affects the coordinate.
Why it is needed: This is Equation (5), the main bridge from Algorithm 1's reward update to the regret-oriented analysis used throughout the paper.
Place in the proof: This finite conditional-mean algebra is the deterministic consumer. A separate compiled process theorem now constructs the recursive history policy and identifies this expression with the generated next-pair history-step-kernel integral under explicit coordinate-update integrability and arm-reward integral equalities.

Proof and Lean reading notes

Proof idea: Split the finite expectation over the selected arm, simplify the selected and nonselected update cases, and rewrite weighted arm means using gap_k = bestMean - mean_k and total probability one.
Lean reading notes: This declaration deliberately consumes a finite probability vector, arm means, and an explicit mean-gap equality. The trajectory module reuses it after separately constructing the SGB state, softmax Markov law, and canonical action/reward trajectory.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.expectedSourceIncrement_eq_gradientCoordinate, BanditRLProof.StochasticGradientBandit.instantaneousGap_eq_bestMean_sub_policyValue

Exact Lean statement

theorem expectedSourceIncrement_eq_gapCoordinate (p mean gap : Action -> Real) (bestMean : Real) (k : Action) (hp : ∑ a, p a = 1) (hgap : ∀ a, gap a = bestMean - mean a) : expectedSourceIncrement p mean k = p k * (instantaneousGap p gap - gap k)

Open in the declaration catalog Open source at line 155

Mathematics ↔ Lean

For the canonical generated SGB process, the conditional next-pair kernel…

Lean declarationBanditRLProof.StochasticGradientBandit.integral_measurableEnvironmentHistoryStepKernel_sourceIncrement_eq_gapCoordinate

Compiled

Plain-English statement. For the canonical generated SGB process, the conditional next-pair kernel integral of the coordinate update equals that coordinate's softmax probability times current expected gap minus the arm's own gap.

Mathematical reading. Formula renderer unavailable; readable fallback: For the canonical generated SGB process, the conditional next-pair kernel integral of the coordinate update equals that coordinate's softmax probability times current expected gap minus the arm's own gap.\(\int \delta\theta_k(a,r)\,K_t(d a,d r\mid e,h)=p_k(h)\bigl(\sum_a p_a(h)\Delta_a-\Delta_k\bigr).\)

Intuition: The static finite sum from Equation (5) is now attached to the actual recursive policy state: the generated softmax law selects the arm, the explicit reward kernel supplies its mean, and the kernel integral performs the conditioning step.
Why it is needed: This closes the main process boundary left by the first audit. It lets later rate arguments consume a generated-history Equation-(5) identity instead of assuming that a deterministic probability vector came from Algorithm 1.
Place in the proof: The recursive state, measurable policies, canonical trajectory, conditional laws, and pointwise Equation-(5) kernel calculation compile. Bounded support supplies update integrability. A downstream two-arm theorem layer now integrates this identity into the expected recursive best parameter and the exact Theorem-1 endpoint; Theorems 2–4 remain open.

Proof and Lean reading notes

Proof idea: Integrate the exact selected/nonselected update through the history-step comp-product kernel, rewrite each reward integral by the selected arm's explicit mean hypothesis, reduce the finite action measure to a softmax-weighted sum, and invoke the compiled gap-coordinate identity.
Lean reading notes: This generic theorem keeps coordinate-update integrability and arm-reward integral equalities explicit. Separate compiled contract wrappers derive the integrability premise from support in [-1,1], and the fixed-IID consumer supplies the source-law specialization.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.measurable_historyParameter, BanditRLProof.StochasticGradientBandit.trajectoryMeasure_condDistrib_nextPair_given_environment_prefix, BanditRLProof.StochasticGradientBandit.expectedSourceIncrement_eq_gapCoordinate

Exact Lean statement

theorem integral_measurableEnvironmentHistoryStepKernel_sourceIncrement_eq_gapCoordinate {Env : Type v} [MeasurableSpace Env] (initialTheta : Action -> Real) (eta : Real) (environment : Thompson.MeasurableHistoryEnvironment Env Action Real) (n : Nat) (env : Env) (history : History.FinitePairHistory Action Real n) (mean gap : Action -> Real) (bestMean : Real) (coordinate : Action) (hIntegrable : Integrable (fun pair : Action × Real => sourceIncrement (softmaxProbability (historyParameter initialTheta eta n history)) pair.2 pair.1 coordinate) (Thompson.measurableEnvironmentHistoryStepKernel (historyAlgorithm initialTheta eta) environment n (env, history))) (hmean : forall selected, integral (environment.feedback n (env, (history, selected))) id = mean selected) (hgap : forall action, gap action = bestMean - mean action) : integral (Thompson.measurableEnvironmentHistoryStepKernel (historyAlgorithm initialTheta eta) environment n (env, history)) (fun pair : Action × Real => sourceIncrement (softmaxProbability (historyParameter initialTheta eta n history)) pair.2 pair.1 coordinate) = softmaxProbability (historyParameter initialTheta eta n history) coordinate * (instantaneousGap (softmaxProbability (historyParameter initialTheta eta n history)) gap - gap coordinate)

Open in the declaration catalog Open source at line 433

Mathematics ↔ Lean

For the fixed two-arm IID source model, bounded rewards automatically make…

Lean declarationBanditRLProof.StochasticGradientBandit.integral_twoArmFixedIIDHistoryStepKernel_sourceIncrement_eq_gapCoordinate

Compiled

Plain-English statement. For the fixed two-arm IID source model, bounded rewards automatically make the generated SGB coordinate update integrable, so the one-step conditional kernel integral equals the Equation-(5) gap coordinate.

Mathematical reading. Formula renderer unavailable; readable fallback: For the fixed two-arm IID source model, bounded rewards automatically make the generated SGB coordinate update integrable, so the one-step conditional kernel integral equals the Equation-(5) gap coordinate.\(\int \delta\theta_k(a,r)\,K_t(d a,d r\mid h)=p_k(h)\bigl(\sum_a p_a(h)\Delta_a-\Delta_k\bigr).\)

Intuition: The source assumes every reward lies in [-1,1]. The softmax update is no larger in absolute value than the observed reward, so no extra moment or independence assumption is needed to justify the conditional integral.
Why it is needed: This removes an artificial caller-supplied regularity premise from the fixed-IID Equation-(5) route and records exactly where bounded support enters the formal proof.
Place in the proof: The fixed-IID one-step Equation-(5) interface compiles. The exact downstream Theorem-1 layer now specializes the whole trajectory to this fixed-IID model with a Dirac prior and assembles Equation (7); Theorems 2–4 remain separate open endpoints.

Proof and Lean reading notes

Proof idea: Transport the armwise support contract through the action/reward comp-product kernel, dominate sourceIncrement by the unit reward envelope, derive Integrable sourceIncrement, and invoke the existing gap-coordinate kernel identity.
Lean reading notes: The theorem reuses the existing probability, bounded-support, integral-mean, and gap-coordinate hypotheses. It adds no positive-gap, learning-rate-sign, second-moment, or independence premise.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.integrable_measurableTwoArmHistoryStepKernel_sourceIncrement_of_contract, BanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironment_contract, BanditRLProof.StochasticGradientBandit.integral_measurableEnvironmentHistoryStepKernel_sourceIncrement_eq_gapCoordinate

Exact Lean statement

theorem integral_twoArmFixedIIDHistoryStepKernel_sourceIncrement_eq_gapCoordinate (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (mean : Fin 2 -> Real) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, |reward| <= 1) (hmean : forall arm, integral (armLaw arm) id = mean arm) (initialTheta : Fin 2 -> Real) (eta : Real) (n : Nat) (history : History.FinitePairHistory (Fin 2) Real n) (gap : Fin 2 -> Real) (bestMean : Real) (coordinate : Fin 2) (hgap : forall action, gap action = bestMean - mean action) : integral (Thompson.measurableEnvironmentHistoryStepKernel (historyAlgorithm initialTheta eta) (twoArmFixedIIDEnvironment armLaw hprob) n ((), history)) (fun pair : Fin 2 × Real => sourceIncrement (softmaxProbability (historyParameter initialTheta eta n history)) pair.2 pair.1 coordinate) = softmaxProbability (historyParameter initialTheta eta n history) coordinate * (instantaneousGap (softmaxProbability (historyParameter initialTheta eta n history)) gap - gap coordinate)

Open in the declaration catalog Open source at line 117

Mathematics ↔ Lean

At every finite source-time prefix of the zero-initialized two-arm SGB…

Lean declarationBanditRLProof.StochasticGradientBandit.twoArmProbabilityAt_zero_div_failure_eq_exp_two_mul

Compiled

Plain-English statement. At every finite source-time prefix of the zero-initialized two-arm SGB process, the best-arm softmax odds equal the exponential of twice its parameter.

Mathematical reading. Formula renderer unavailable; readable fallback: At every finite source-time prefix of the zero-initialized two-arm SGB process, the best-arm softmax odds equal the exponential of twice its parameter.\(p_{1,t}/(1-p_{1,t})=e^{2\theta_{1,t}}.\)

Intuition: The Algorithm-1 updates preserve the sum of the two parameters. Starting from zero therefore makes the coordinates opposites, so the two-arm softmax ratio collapses to one exponential coordinate.
Why it is needed: This is the printed Equation (11) used to turn exponential-parameter recurrences into probability statements in the proof of Theorem 1.
Place in the proof: The exact pathwise odds identity and its multiplication forms compile. No conditional exponential recurrence, expected squared failure-mass bound, or Theorem-1 regret inequality follows from this identity alone.

Proof and Lean reading notes

Proof idea: Prove the recursive parameter-sum invariant on inclusive histories, specialize zero initialization, identify the two coordinates as negatives, and cancel the positive softmax denominator.
Lean reading notes: Lean time zero is source time one before any update; Lean time n+1 consumes exactly trace pair n. Lean arm zero corresponds to source arm one.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.twoArmParameterAt_sum_eq_zero, BanditRLProof.StochasticGradientBandit.softmaxProbability_zero_div_one_sub_zero_eq_exp_two_mul

Exact Lean statement

theorem twoArmProbabilityAt_zero_div_failure_eq_exp_two_mul (eta : Real) (trace : Nat -> Fin 2 × Real) (time : Nat) : twoArmProbabilityAt eta trace time 0 / (1 - twoArmProbabilityAt eta trace time 0) = Real.exp (2 * twoArmParameterAt eta trace time 0)

Open in the declaration catalog Open source at line 222

Mathematics ↔ Lean

For any probability law and almost-everywhere measurable reward supported…

Lean declarationBanditRLProof.StochasticGradientBandit.integral_exp_mul_le_sourceEqEight_of_ae_abs_le_one

Compiled

Plain-English statement. For any probability law and almost-everywhere measurable reward supported on [-1, 1], its exponential moment obeys the source's exact second-order C-eta bound.

Mathematical reading. Formula renderer unavailable; readable fallback: For any probability law and almost-everywhere measurable reward supported on [-1, 1], its exponential moment obeys the source's exact second-order C-eta bound.\(\mathbb E[e^{qR}]\le 1+q\mathbb E[R]+\tfrac{q^2}{2}C_{|q|/2}.\)

Intuition: After the constant and linear terms, every higher Taylor coefficient is controlled by replacing the bounded reward with its absolute worst case. The shifted exponential series is exactly the paper's C-eta constant.
Why it is needed: This compiles Equation (8), the moment-generating-function estimate that drives both conditional exponential recurrences in the two-arm Theorem-1 proof.
Place in the proof: This remains the standalone generic probability-law layer. Separate compiled declarations now instantiate it on the generated initial/successor reward kernels and feed the two-arm recurrence route; the generic theorem itself is not relabelled as a trajectory theorem.

Proof and Lean reading notes

Proof idea: Split the exponential series into constant, linear, and degree-at-least-two terms; dominate the tail using |qR| <= |q|; then integrate the pointwise bound and derive integrability from measurability and bounded support.
Lean reading notes: The theorem requires only a probability measure, almost-everywhere strong measurability, and |R| <= 1 almost everywhere. Independence is not needed for Equation (8); it enters only through later trajectory/kernel instantiation.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.sourceC_terms_summable, BanditRLProof.StochasticGradientBandit.sq_div_two_mul_sourceC_abs_div_two, BanditRLProof.StochasticGradientBandit.exp_mul_le_sourceEqEight

Exact Lean statement

theorem integral_exp_mul_le_sourceEqEight_of_ae_abs_le_one {Omega : Type*} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] (q : Real) (reward : Omega -> Real) (hrewardMeasurable : MeasureTheory.AEStronglyMeasurable reward mu) (hreward : ∀ᵐ omega ∂mu, |reward omega| <= 1) : (∫ omega, Real.exp (q * reward omega) ∂mu) <= 1 + q * (∫ omega, reward omega ∂mu) + q ^ 2 / 2 * sourceC (|q| / 2)

Open in the declaration catalog Open source at line 193

Mathematics ↔ Lean

Along the canonical two-arm SGB trajectory, the conditional-distribution…

Lean declarationBanditRLProof.StochasticGradientBandit.trajectoryPrefix_condDistrib_integral_forwardSuccessor_le

Compiled

Plain-English statement. Along the canonical two-arm SGB trajectory, the conditional-distribution integral of the next forward exponential potential obeys the source-shaped one-step recurrence at almost every observed prefix.

Mathematical reading. Formula renderer unavailable; readable fallback: Along the canonical two-arm SGB trajectory, the conditional-distribution integral of the next forward exponential potential obeys the source-shaped one-step recurrence at almost every observed prefix.\(\int e^{2\theta_{1,t+1}}\,dK_t\le e^{2\theta_{1,t}}+2p_t^2(\eta\Delta+\eta^2C_\eta).\)

Intuition: Equation (8) is now attached to the actual generated next-pair law. The softmax update determines the exponential coefficient, while bounded support and fixed arm means control the reward moment.
Why it is needed: This is the measurable trajectory bridge between the fixed-history recurrence algebra and a conditional-expectation argument on the generated process.
Place in the proof: The forward and inverse a.e. conditional-distribution transports compile under the explicit bounded fixed-mean environment contract. With a general prior the prefix reveals the latent environment; a fixed/Dirac environment gives the fixed-instance reading.

Proof and Lean reading notes

Proof idea: Prove the fixed-history kernel inequality, identify the canonical successor conditional distribution at the environment/prefix input, and transport the integral inequality almost everywhere.
Lean reading notes: The contract fixes support in [-1,1] and arm means at every fiber, but is not an equivalent encoding of a fixed-iid reward law. This conditional-distribution theorem is only one step; the separate unconditional module supplies finite iteration and the generic failure-mass sum.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.TwoArmBoundedFixedMeanEnvironmentContract, BanditRLProof.StochasticGradientBandit.integral_measurableTwoArmHistoryStepKernel_forwardSuccessor_le_of_contract, BanditRLProof.StochasticGradientBandit.trajectoryMeasure_condDistrib_nextPair_given_environment_prefix

Exact Lean statement

theorem trajectoryPrefix_condDistrib_integral_forwardSuccessor_le {Env : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] (prior : Measure Env) [IsFiniteMeasure prior] (eta Delta : Real) (heta : 0 <= eta) (environment : Thompson.MeasurableHistoryEnvironment Env (Fin 2) Real) (mean : Fin 2 -> Real) (contract : TwoArmBoundedFixedMeanEnvironmentContract environment mean) (hgap : mean 0 - mean 1 = Delta) (n : Nat) : ∀ᵐ context ∂(twoArmTrajectoryMeasure prior eta environment).map (twoArmEnvironmentPrefix n), integral (condDistrib (twoArmNextPair n) (twoArmEnvironmentPrefix n) (twoArmTrajectoryMeasure prior eta environment) context) (twoArmForwardSuccessorPotential eta context.2) <= twoArmForwardRecurrenceBound eta Delta context.2

Open in the declaration catalog Open source at line 430

Mathematics ↔ Lean

For each fixed finite time, the forward exponential potential is integrable…

Lean declarationBanditRLProof.StochasticGradientBandit.twoArmForwardTrajectorySuccessor_condExp_le_recurrenceBound

Compiled

Plain-English statement. For each fixed finite time, the forward exponential potential is integrable and its conditional expectation is bounded by the measurable source recurrence bound.

Mathematical reading. Formula renderer unavailable; readable fallback: For each fixed finite time, the forward exponential potential is integrable and its conditional expectation is bounded by the measurable source recurrence bound.\(\mathbb E[e^{2\theta_{1,t+1}}\mid\mathcal F_t]\le e^{2\theta_{1,t}}+2p_t^2(\eta\Delta+\eta^2C_\eta)\quad\text{a.e.}\)

Intuition: Finite-prefix reward support bounds every recursive parameter, which makes the exponential potential integrable. Conditional-distribution uniqueness then turns the compiled kernel integral into a genuine one-step conditional expectation.
Why it is needed: This closes the fixed-horizon integrability and condexp boundary needed before a tower argument can iterate the recurrence.
Place in the proof: Forward and inverse tower-ready one-step bounds compile. The unconditional and Theorem-1 layers now integrate them, perform finite iteration, prove the squared failure-mass bound, and consume the forward recurrence through Jensen/log in the exact two-arm fixed-IID endpoint.

Proof and Lean reading notes

Proof idea: Transport bounded rewards to every prefix, bound the history parameter by the accumulated reward magnitudes, prove exponential integrability, identify condexp with the conditional-distribution integral, and apply the a.e. recurrence transport.
Lean reading notes: This theorem itself is fixed-time and one-step. The downstream Theorem-1 module supplies the finite-horizon Jensen/log consumer only for the exact two-arm fixed-IID/Dirac source contract; the learning-rate rates in Theorems 2–4 remain absent.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.integrable_twoArmForwardTrajectorySuccessorPotential, BanditRLProof.StochasticGradientBandit.twoArmForwardTrajectorySuccessor_condExp_ae_eq_integral_condDistrib, BanditRLProof.StochasticGradientBandit.trajectoryPrefix_condDistrib_integral_forwardSuccessor_le

Exact Lean statement

theorem twoArmForwardTrajectorySuccessor_condExp_le_recurrenceBound {Env : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] (prior : Measure Env) [IsFiniteMeasure prior] (eta Delta : Real) (heta : 0 <= eta) (environment : Thompson.MeasurableHistoryEnvironment Env (Fin 2) Real) (mean : Fin 2 -> Real) (contract : TwoArmBoundedFixedMeanEnvironmentContract environment mean) (hgap : mean 0 - mean 1 = Delta) (n : Nat) : (twoArmTrajectoryMeasure prior eta environment)[ fun sample : Env × ((k : Nat) -> Fin 2 × Real) => twoArmForwardSuccessorPotential eta (twoArmEnvironmentPrefix n sample).2 (twoArmNextPair n sample) | twoArmPrefixSigma (Env := Env) n] ≤ᵐ[ twoArmTrajectoryMeasure prior eta environment] fun sample : Env × ((k : Nat) -> Fin 2 × Real) => twoArmForwardRecurrenceBound eta Delta (twoArmEnvironmentPrefix n sample).2

Open in the declaration catalog Open source at line 676

Mathematics ↔ Lean

For the source-initialized two-arm process, a positive learning rate and…

Lean declarationBanditRLProof.StochasticGradientBandit.twoArmFullFailureMassSqSum_le

Compiled

Plain-English statement. For the source-initialized two-arm process, a positive learning rate and the strict margin eta C-eta < Delta bound the first-round failure square plus every expected squared later failure probability by one explicit reciprocal coefficient.

Mathematical reading. Formula renderer unavailable; readable fallback: For the source-initialized two-arm process, a positive learning rate and the strict margin eta C-eta < Delta bound the first-round failure square plus every expected squared later failure probability by one explicit reciprocal coefficient.\(\frac14+\sum_{n=0}^{N-1}\mathbb E[(1-p_{1,n+2})^2]\le\frac{1}{2\eta(\Delta-\eta C_\eta)}.\)

Intuition: The inverse odds potential loses a positive multiple of squared failure mass at every step and remains nonnegative at the terminal horizon. Zero initialization makes the source-round-1 failure exactly 1/2, so its square contributes 1/4.
Why it is needed: This closes the generic unconditional recurrence and expected squared failure-mass node that was previously open after the tower-ready one-step inequalities.
Place in the proof: This reusable declaration holds on a generic bounded fixed-mean trajectory with a probability prior. A downstream theorem now specializes it to the fixed-IID/Dirac source model and closes Equation (7) and Theorem 1; this generic declaration alone is not that endpoint.

Proof and Lean reading notes

Proof idea: Integrate the inverse conditional recurrence, telescope the finite scalar sequence, prove the coefficient 2 eta (Delta - eta C-eta) positive, use terminal exponential nonnegativity, and combine the normalized initial inverse recurrence with the exact coefficient-times-1/4 identity.
Lean reading notes: Lean index n has consumed trace coordinates 0 through n and represents source probability p_{1,n+2}. Finset.range N therefore covers source rounds 2 through N+1; the explicit 1/4 supplies source round 1.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.twoArmInverseFailureMassSqTelescope, BanditRLProof.StochasticGradientBandit.twoArmInverseInitialUnconditionalRecurrence, BanditRLProof.StochasticGradientBandit.integrable_twoArmFailureMass_sq

Exact Lean statement

theorem twoArmFullFailureMassSqSum_le {Env : Type v} [MeasurableSpace Env] [StandardBorelSpace Env] (prior : Measure Env) [IsProbabilityMeasure prior] (eta Delta : Real) (heta : 0 < eta) (environment : Thompson.MeasurableHistoryEnvironment Env (Fin 2) Real) (mean : Fin 2 -> Real) (contract : TwoArmBoundedFixedMeanEnvironmentContract environment mean) (hgap : mean 0 - mean 1 = Delta) (hmargin : eta * sourceC eta < Delta) (tailHorizon : Nat) : (1 : Real) / 4 + (Finset.range tailHorizon).sum (fun n => integral (twoArmTrajectoryMeasure prior eta environment) (fun sample => twoArmFailureMass (Env := Env) eta n sample ^ 2)) <= 1 / (2 * eta * (Delta - eta * sourceC eta))

Open in the declaration catalog Open source at line 812

Mathematics ↔ Lean

Under explicit positive minimum-gap and maximum-gap envelopes, finite…

Lean declarationBanditRLProof.StochasticGradientBandit.sourceRegretDecomposition_le

Compiled

Plain-English statement. Under explicit positive minimum-gap and maximum-gap envelopes, finite expected pseudo-regret is bounded by a best-parameter post-convergence term plus squared failure mass.

Mathematical reading. Formula renderer unavailable; readable fallback: Under explicit positive minimum-gap and maximum-gap envelopes, finite expected pseudo-regret is bounded by a best-parameter post-convergence term plus squared failure mass.\(R_T\le \frac{\Delta_{\max}}{\eta\Delta}\,\Theta_{1,T+1}+\Delta_{\max}\sum_{t<T}(1-p_{1,t})^2.\)

Intuition: The identity 1-p = p(1-p)+(1-p)^2 separates rounds where the best coordinate can accumulate useful drift from trajectories that keep too much probability away from the best arm.
Why it is needed: This is the deterministic mechanism behind Equation (7) and makes the paper's later learning-rate question visible as a separate failure-mass problem.
Place in the proof: The source-shaped finite decomposition compiles. The exact downstream two-arm trajectory theorem now identifies the expected best parameter, proves the forward Jensen/log and failure-mass bounds, aligns the source horizon, and closes Theorem 1. Theorems 2–4 remain uncompiled.

Proof and Lean reading notes

Proof idea: Upper-bound each instantaneous gap by DeltaMax times failure mass, lower-bound the best-coordinate increment using the minimum gap, split failure mass algebraically, and divide only after proving eta*Delta positive.
Lean reading notes: Theta is represented here by a finite sum of history-conditioned expected best-coordinate increments. The compiled Theorem-1 layer separately identifies the corresponding generated expected recursive parameter and then bridges generated regret to actual sampled-action regret.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.bestParameterIncrementSum_ge, BanditRLProof.StochasticGradientBandit.instantaneousGap_le_maxGap_mul_failureMass, BanditRLProof.StochasticGradientBandit.failureMass_eq_successFailure_add_sq

Exact Lean statement

theorem sourceRegretDecomposition_le (eta Delta DeltaMax : Real) (p : Nat -> Action -> Real) (gap : Action -> Real) (best : Action) (horizon : Nat) (heta : 0 < eta) (hDelta : 0 < Delta) (hDeltaMax : 0 <= DeltaMax) (hp : ∀ t, ∑ a, p t a = 1) (hp_nonneg : ∀ t a, 0 <= p t a) (hgap_best : gap best = 0) (hgap_min : ∀ a, a ≠ best -> Delta <= gap a) (hgap_max : ∀ a, a ≠ best -> gap a <= DeltaMax) : sourceExpectedPseudoRegret p gap horizon <= (DeltaMax / (eta * Delta)) * bestParameterIncrementSum eta p gap best horizon + DeltaMax * (∑ t ∈ Finset.range horizon, (1 - p t best) ^ 2)

Open in the declaration catalog Open source at line 302

Mathematics ↔ Lean

For every horizon at least two, the generated zero-initialized two-arm…

Lean declarationBanditRLProof.StochasticGradientBandit.twoArmFixedIIDDirac_corollaryOne

Compiled

Plain-English statement. For every horizon at least two, the generated zero-initialized two-arm fixed-IID SGB trajectory with learning rate sqrt(log T / T) has expected sampled pseudo-regret at most an explicit absolute constant times sqrt(T log T).

Mathematical reading. Formula renderer unavailable; readable fallback: For every horizon at least two, the generated zero-initialized two-arm fixed-IID SGB trajectory with learning rate sqrt(log T / T) has expected sampled pseudo-regret at most an explicit absolute constant times sqrt(T log T).\(\mathbb E R_T^{\mathrm{SGB}}\le\left(2+\frac1{\log 2}+2e^2\right)\sqrt{T\log T},\qquad T\ge2.\)

Intuition: When the learning rate is small relative to the gap, the compiled Theorem-1 bound supplies the rate. On the complementary branch, failure of that margin makes the trivial pathwise Delta T bound no larger than the same square-root scale.
Why it is needed: This turns the source Corollary-1 asymptotic statement into a finite, constant-explicit theorem about the actual sampled actions, while keeping its dependence on the already compiled Theorem 1 visible.
Place in the proof: This is a compiled bounded companion and direct Theorem-1 consumer. It is not evidence for the polynomial-regret Theorem 2, a time-varying policy, or general K.

Proof and Lean reading notes

Proof idea: Define one fixed eta_T for each horizon, prove positivity and the eta-times-horizon square-root identity, simplify the Theorem-1 constant on its valid branch, use the pathwise Delta T bound otherwise, and dominate both branches by one horizon-independent constant.
Lean reading notes: The theorem retains T >= 2, 0 < Delta < 1, bounded fixed-IID reward laws, exact arm means, source zero initialization, and T = tailHorizon + 1. Measure.dirac () is the prior on the singleton Unit environment; it does not assert that either reward law is Dirac or Rademacher.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.twoArmFixedIIDDirac_corollaryOne_piecewise, BanditRLProof.StochasticGradientBandit.corollaryOne_piecewise_bound, BanditRLProof.StochasticGradientBandit.twoArmFixedIIDDirac_theoremOne

Exact Lean statement

theorem twoArmFixedIIDDirac_corollaryOne (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (mean : Fin 2 -> Real) (hbound : forall arm, ∀ᵐ reward ∂armLaw arm, |reward| <= 1) (hmean : forall arm, integral (armLaw arm) id = mean arm) (Delta : Real) (hDelta : 0 < Delta) (hDelta_lt_one : Delta < 1) (hgap : mean 0 - mean 1 = Delta) (tailHorizon : Nat) (horizon_ge_two : 1 <= tailHorizon) : let eta := corollaryOneEta (tailHorizon + 1) integral (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) (twoArmSampledPseudoRegret (Env := Unit) Delta (tailHorizon + 1)) <= corollaryOneAbsoluteConstant * corollaryOneRate (tailHorizon + 1)

Open in the declaration catalog Open source at line 468

Mathematics ↔ Lean

If the zero-based k-th optimal-arm pull occurs at chronological coordinate…

Lean declarationBanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullTime_spec

Compiled

Plain-English statement. If the zero-based k-th optimal-arm pull occurs at chronological coordinate t, then exactly k optimal pulls occurred earlier, action t is arm 0, and the inclusive count through t is k plus one.

Mathematical reading. Formula renderer unavailable; readable fallback: If the zero-based k-th optimal-arm pull occurs at chronological coordinate t, then exactly k optimal pulls occurred earlier, action t is arm 0, and the inclusive count through t is k plus one.\(\tau_k=t\Longrightarrow N_0(t)=k,\quad A_t=0,\quad N_0(t+1)=k+1.\)

Intuition: Appendix C reasons in the order in which the optimal arm is pulled, while the generated Lean trajectory is ordered by wall-clock rounds. The stopping time is the dictionary between those two clocks.
Why it is needed: The source proof uses an implicit pull-indexed reward chain. Making the missing-pull case, stopping boundary, and exact off-by-one convention explicit prevents a fixed chronological cutoff from being mistaken for the random n-th pull.
Place in the proof: This is a compiled chronological nth-pull bridge required by the frozen Theorem-2 route. It is formalization infrastructure rather than a stopping-time theorem quoted from the source, and it does not close Appendix-C Step 1 or Theorem 2.

Proof and Lean reading notes

Proof idea: Factor the inclusive pull count through the canonical finite-prefix filtration, apply Mathlib's hitting-time construction with an explicit WithTop value, and use the one-step pull-count recurrence plus minimality of the hit to recover the selected action and exact before/after counts.
Lean reading notes: The pullIndex argument is zero based. At top, Mathlib totalizes stoppedValue through untopA, so the reward and probability identification lemmas require a finite-time witness. Separate compiled layers now supply a fixed-arm finite product law, finite-pull coordinate readout, and a deferred-decisions finite-prefix mixture; this inclusive stopping-time theorem alone supplies none of them, and the mixture's visible marginal has not been identified with the native fixed-IID prefix law.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.isStoppingTime_twoArmNthOptimalPullTime, BanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullTime_eq_top_iff, BanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullReward_eq_of_time_eq, BanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullSuccessProbability_eq_of_time_eq

Exact Lean statement

theorem twoArmNthOptimalPullTime_spec {Env : Type v} [MeasurableSpace Env] (pullIndex t : Nat) (sample : Env × ((k : Nat) -> Fin 2 × Real)) (htime : twoArmNthOptimalPullTime pullIndex sample = (t : WithTop Nat)) : twoArmOptimalPullCount t sample = pullIndex /\ twoArmGeneratedAction sample t = 0 /\ twoArmOptimalPullCount (t + 1) sample = pullIndex + 1

Open in the declaration catalog Open source at line 262

Mathematics ↔ Lean

For every finite length m, the first m latent rewards of the optimal arm in…

Lean declarationBanditRLProof.StochasticGradientBandit.twoArmFixedIIDLatentTrajectoryMeasure_map_optimalPrefix_eq_pi

Compiled

Plain-English statement. For every finite length m, the first m latent rewards of the optimal arm in the coupled two-arm fixed-IID SGB construction have exactly the m-fold product of that arm's reward law.

Mathematical reading. Formula renderer unavailable; readable fallback: For every finite length m, the first m latent rewards of the optimal arm in the coupled two-arm fixed-IID SGB construction have exactly the m-fold product of that arm's reward law.\(\mathcal L((Z_{i,0})_{i<m})=\bigotimes_{i<m}\nu_0.\)

Intuition: The coupling gives each arm an infinite private stream of fresh rewards. Adaptive actions decide when a coordinate is consumed, but they do not change the unconditional product law of the latent coordinates themselves.
Why it is needed: Appendix C groups rewards by optimal-arm pull count. This theorem makes the independent finite reward blocks explicit before any ballot or anti-concentration calculation is attempted.
Place in the proof: This is a compiled latent-law producer, not the native selected-reward theorem or Theorem 2. Separate compiled theorems give finite nth-pull readout, finite stream-box factorization, target-by-target branch locality, deterministic-time one-step selected-reward freshness, and equality with the native process at every finite visible prefix. Full trajectory-law transport and stopped pull-ordered blocks remain open.

Proof and Lean reading notes

Proof idea: Restrict the mutually independent time-arm coordinate family to the injective finite index map i maps to (i,0), use Mathlib's equivalence between finite independence and a product pushforward, identify each coordinate marginal, and lift the result through the coupling's exact stream marginal.
Lean reading notes: The theorem does not totalize missing pulls, condition on all requested pulls occurring, or assert full infinite-trajectory equality between the coupling's visible marginal and the canonical Unit-environment fixed-IID SGB law. A downstream module proves equality only after every finite-prefix projection. Those distinctions prevent a stopping-dependent selection event from being silently treated as independent.
Teaching dependencies: BanditRLProof.UCB.armStreamMeasure_map_fixedArmFinitePrefix_eq_pi, BanditRLProof.Thompson.latentArmStreamTrajectoryMeasure_map_fixedArmFinitePrefix_eq_pi, BanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullReward_eq_latentCoordinate_ae

Exact Lean statement

theorem twoArmFixedIIDLatentTrajectoryMeasure_map_optimalPrefix_eq_pi (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) (m : Nat) : Measure.map (fun sample : UCB.ArmRewardStream 2 × ((n : Nat) -> Fin 2 × Real) => fun i : Fin m => sample.1 (i : Nat) 0) (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta) = Measure.pi (fun _ : Fin m => armLaw 0)

Open in the declaration catalog Open source at line 183

Mathematics ↔ Lean

At every finite cutoff, the joint law of the latent reward stream box and…

Lean declarationBanditRLProof.Thompson.latentArmStreamTrajectoryMeasure_map_stream_visiblePrefix_eq

Compiled

Plain-English statement. At every finite cutoff, the joint law of the latent reward stream box and generated visible history prefix is exactly the product stream-box law followed by a Markov visible-prefix kernel.

Mathematical reading. Formula renderer unavailable; readable fallback: At every finite cutoff, the joint law of the latent reward stream box and generated visible history prefix is exactly the product stream-box law followed by a Markov visible-prefix kernel.\(\mathcal L(Z_{\le n},H_{\le n})=\left(\bigotimes_{t\le n}\bigotimes_a\nu_a\right)\ltimes K_n^{\mathrm{vis}}.\)

Intuition: The algorithm can adapt its actions to rewards already revealed, but its visible history through round n cannot depend on latent reward coordinates after n. The proof makes that deferred-decisions boundary explicit without pretending that actions are deterministic or independent.
Why it is needed: This isolates the exact finite joint mixture whose visible marginal a native-trajectory adapter must identify. It prevents the stronger native law from being smuggled in through an informal coupling argument.
Place in the proof: This eight-declaration finite-prefix factorization is compiled. A downstream ten-declaration native-law module now identifies every finite prefix and promotes those identities to equality of the complete visible/native trajectory measures. Theorem 2 remains unproved.

Proof and Lean reading notes

Proof idea: Map the infinite arm-stream product to its inclusive finite restriction, prove equality of the canonical generated prefix laws under equal stream boxes, package that kernel-law locality as a Markov prefix kernel, and map the stream/trajectory compProd through both restrictions.
Lean reading notes: The cutoff n is inclusive, so the stream box contains coordinates 0 through n for every arm. The right side is a kernel mixture, not an independence assertion between the latent box and visible prefix. Target-by-target branch products, deterministic-time one-step aggregation, finite native-prefix identification, and full visible/native trajectory-law transport now compile. Stopped selected-IID transport and the future-cylinder law remain unproved.
Teaching dependencies: BanditRLProof.UCB.armStreamMeasure_map_frestrictLe_eq_pi, BanditRLProof.Thompson.latentArmStreamTrajectoryKernel_map_frestrictLe_eq_of_streamPrefix_eq, BanditRLProof.Thompson.latentArmStreamTrajectoryKernel_map_frestrictLe_eq_prefixKernel_comap

Exact Lean statement

theorem latentArmStreamTrajectoryMeasure_map_stream_visiblePrefix_eq {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : Measure.map (fun sample : UCB.ArmRewardStream K × ((t : Nat) -> Fin K × Real) => (Preorder.frestrictLe n sample.1, Preorder.frestrictLe n sample.2)) (latentArmStreamTrajectoryMeasure algorithm env nu) = Measure.pi (fun _ : Finset.Iic n => Measure.infinitePi fun arm : Fin K => nu arm) ⊗ₘ latentArmStreamVisiblePrefixKernel algorithm env n

Open in the declaration catalog Open source at line 1629

Mathematics ↔ Lean

After the latent reward stream is mixed out, the joint law of the visible…

Lean declarationBanditRLProof.Thompson.latentArmStreamTrajectoryMeasure_map_visiblePrefix_nextAction_eq_compProd

Compiled

Plain-English statement. After the latent reward stream is mixed out, the joint law of the visible prefix through n and the action selected at n plus one is the visible-prefix marginal followed by the algorithm's policy kernel at n.

Mathematical reading. Formula renderer unavailable; readable fallback: After the latent reward stream is mixed out, the joint law of the visible prefix through n and the action selected at n plus one is the visible-prefix marginal followed by the algorithm's policy kernel at n.\(\mathcal L(H_{\le n},A_{n+1})=\mathcal L(H_{\le n})\ltimes\pi_n.\)

Intuition: The latent stream changes how rewards are coupled, not how the algorithm randomizes its next action once the visible history is fixed. This theorem isolates that action half of the one-step law.
Why it is needed: A native-trajectory adapter must separate next-action randomization from selected-reward freshness. Proving the action factorization first leaves the genuine deferred-decisions obligation visible instead of hiding it inside a larger kernel equality.
Place in the proof: This is an unconditional compiled theorem in the 13-declaration action/readout and branch-locality-interface scaffold. It is not a selected-reward freshness theorem, native trajectory-law identification, or Theorem 2.

Proof and Lean reading notes

Proof idea: Apply the generic trajectory-mixture action-law transport to each fixed latent stream, use the canonical history algorithm's policy law at the shifted successor coordinate, and then mix the stream out.
Lean reading notes: A separate compiled almost-sure theorem identifies the observed next reward with the selected latent coordinate. The count-capped restricted-measure induction proves LatentArmStreamVisiblePrefixNextActionBranchLocality, and a later countable aggregation theorem now closes deterministic-time one-step freshness. Selected IID and native-process identification remain open.
Teaching dependencies: BanditRLProof.Thompson.latentArmStreamTrajectoryMeasure, BanditRLProof.Thompson.latentArmStreamVisiblePrefixNextAction, BanditRLProof.Thompson.trajectoryMixture_map_history_action_eq_compProd, BanditRLProof.Thompson.canonicalMeasurableEnvironmentTrajectoryKernel_map_history_action_eq_compProd

Exact Lean statement

theorem latentArmStreamTrajectoryMeasure_map_visiblePrefix_nextAction_eq_compProd {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : Measure.map (fun sample : UCB.ArmRewardStream K × ((t : Nat) -> Fin K × Real) => latentArmStreamVisiblePrefixNextAction n sample.2) (latentArmStreamTrajectoryMeasure algorithm env nu) = Measure.map (fun sample : UCB.ArmRewardStream K × ((t : Nat) -> Fin K × Real) => Preorder.frestrictLe n sample.2) (latentArmStreamTrajectoryMeasure algorithm env nu) ⊗ₘ algorithm.policy n

Open in the declaration catalog Open source at line 1060

Mathematics ↔ Lean

On the branch where the next selected reward coordinate is a fixed target…

Lean declarationBanditRLProof.Thompson.latentArmStreamVisiblePrefixNextAction_coordinate_branch_eq_prod

Compiled

Plain-English statement. On the branch where the next selected reward coordinate is a fixed target, the visible prefix and next action factor from that target reward coordinate with exactly the selected arm's reward law.

Mathematical reading. Formula renderer unavailable; readable fallback: On the branch where the next selected reward coordinate is a fixed target, the visible prefix and next action factor from that target reward coordinate with exactly the selected arm's reward law.\(\mathcal L((H_{\le n},A_{n+1}),Z_q;\,Q_{n+1}=q)=\mathcal L(H_{\le n},A_{n+1};\,Q_{n+1}=q)\otimes\nu_{q_2}.\)

Intuition: Before coordinate q is consumed, the history may reveal many other latent rewards but not q itself. Restricting to the exact next-coordinate branch therefore leaves q fresh, even though the action policy is adaptive.
Why it is needed: This is the deferred-decisions bridge that the preceding interface only stated as a contract. The later aggregation layer consumes it by summing the disjoint coordinate branches and combining the result with pathwise reward readout.
Place in the proof: This is an unconditional compiled branchwise product law in the 28-declaration branch-locality producer layer. A separate compiled theorem now aggregates all branches into deterministic-time one-step freshness; this branch theorem is still not native fixed-IID trajectory identification, selected IID, or Theorem 2.

Proof and Lean reading notes

Proof idea: Prove fixed-stream prefix laws equal on the pull-count cap by induction. The successor step transports a restricted semidirect product through safe fibers: below the target count every action is safe, while at equality the target arm is excluded. Rebuild the omitted coordinate, restrict to the exact branch, and apply latent-coordinate independence.
Lean reading notes: The branch law is finite/sub-Markov because it is restricted to one coordinate-selection event. The generic safe-fiber compProd lemmas are reusable measure-theoretic infrastructure. Countable aggregation now proves one-step freshness, but no IID or native-process claim follows from that local conditional law.
Teaching dependencies: BanditRLProof.Measure.map_compProd_restrict_eq_of_base_restrict_eq_of_fiber_restrict_eq, BanditRLProof.Thompson.latentArmStreamTrajectoryKernel_map_frestrictLe_restrict_countCap_eq_of_withoutCoordinate_eq, BanditRLProof.Thompson.latentArmStreamVisiblePrefixNextActionBranchLocality, BanditRLProof.UCB.armStreamMeasure_map_output_coordinate_compProd_comap_without_eq_prod

Exact Lean statement

theorem latentArmStreamVisiblePrefixNextAction_coordinate_branch_eq_prod {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) (target : Nat × Fin K) : let branchKernel := ((latentArmStreamTrajectoryKernel algorithm env).map (latentArmStreamVisiblePrefixNextAction n)).restrict (UCB.measurableSet_armStreamHistoryActionCoordinateBranch n target) Measure.map (fun sample : UCB.ArmRewardStream K × (History.FinitePairHistory (Fin K) Real n × Fin K) => (sample.2, UCB.armStreamCoordinate target sample.1)) (UCB.armStreamMeasure nu ⊗ₘ branchKernel) = (Measure.map Prod.snd (UCB.armStreamMeasure nu ⊗ₘ branchKernel)).prod (nu target.2)

Open in the declaration catalog Open source at line 1033

Mathematics ↔ Lean

Under the visible marginal of the latent SGB coupling, once the observed…

Lean declarationBanditRLProof.Thompson.latentArmStreamVisibleTrajectoryMeasure_nextReward_condDistrib_ae_eq_nu

Compiled

Plain-English statement. Under the visible marginal of the latent SGB coupling, once the observed history through n and the action chosen for round n plus one are known, the next reward has exactly the stationary law of that chosen arm.

Mathematical reading. Formula renderer unavailable; readable fallback: Under the visible marginal of the latent SGB coupling, once the observed history through n and the action chosen for round n plus one are known, the next reward has exactly the stationary law of that chosen arm.\(\mathcal L(R_{n+1}\mid H_{\le n},A_{n+1})=\nu_{A_{n+1}}\quad\text{a.e.}\)

Intuition: Adaptive actions may depend on every reward seen so far, but the latent coordinate consumed next has not been exposed. Partitioning by its pull count and arm makes that freshness explicit and then recombines the branches without normalizing them.
Why it is needed: This closes the exact one-step probabilistic interface needed before comparing the latent visible process with the native fixed-IID construction. It is stronger than pathwise reward readout and weaker than a selected-reward IID sequence theorem.
Place in the proof: This is the terminal theorem of an eight-declaration compiled aggregation/readout layer. A downstream ten-declaration module now closes native-prefix identification and complete visible/native trajectory-law equality. Stopped pull-ordered reward blocks, future/no-return, and Theorem 2 remain blocked.

Proof and Lean reading notes

Proof idea: Prove dynamic coordinate evaluation measurable; restrict to each count/arm branch and use the fixed-coordinate product law; sum the countable branch partition on both sides; transport the joint law through the latent coupling; replace the selected coordinate by the actual reward almost everywhere; then invoke the joint-law characterization of condDistrib.
Lean reading notes: The condition is the inclusive visible prefix through n paired with the action at n+1. The selected kernel is nu composed with the action projection. Branch kernels are finite/sub-Markov, and no statement here identifies the visible marginal with the native trajectory or makes rewards at multiple selected times IID.
Teaching dependencies: BanditRLProof.Thompson.latentArmStreamVisiblePrefixNextAction_selectedCoordinate_mixed_eq_compProd, BanditRLProof.Thompson.latentArmStreamVisibleNextReward_eq_selectedCoordinate_ae, BanditRLProof.Thompson.latentArmStreamVisibleNextReward_joint_eq_compProd, BanditRLProof.UCB.armStreamSelectedRewardKernel

Exact Lean statement

theorem latentArmStreamVisibleTrajectoryMeasure_nextReward_condDistrib_ae_eq_nu {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : let visibleMeasure := (latentArmStreamTrajectoryMeasure algorithm env nu).map Prod.snd condDistrib (latentArmStreamVisibleNextReward n) (latentArmStreamVisiblePrefixNextAction n) visibleMeasure =ᵐ[ visibleMeasure.map (latentArmStreamVisiblePrefixNextAction n)] UCB.armStreamSelectedRewardKernel n nu

Open in the declaration catalog Open source at line 1604

Mathematics ↔ Lean

Forgetting the latent reward stream from the coupled SGB construction gives…

Lean declarationBanditRLProof.Thompson.latentArmStreamVisibleTrajectoryMeasure_eq_native

Compiled

Plain-English statement. Forgetting the latent reward stream from the coupled SGB construction gives exactly the same complete visible trajectory law as the native fixed-IID SGB process.

Mathematical reading. Formula renderer unavailable; readable fallback: Forgetting the latent reward stream from the coupled SGB construction gives exactly the same complete visible trajectory law as the native fixed-IID SGB process.\(\mathcal L(H^{\mathrm{latent\;visible}})=\mathcal L(H^{\mathrm{native}}).\)

Intuition: The latent construction pre-samples all arm rewards, while the native process samples only the selected arm. Once every finite observed prefix has the same law, no measurable event of the infinite visible trajectory can distinguish the two processes.
Why it is needed: This closes the process-law transport needed before source Appendix-C reward blocks can be moved from the latent coupling to the native algorithm. It removes a genuine trajectory-semantics blocker without assuming adaptive selected rewards are IID.
Place in the proof: This project-local theorem is compiled in a separate ten-declaration native-law module. It proves complete visible/native measure equality, not stopped or pull-ordered selected-reward IID, a random-time future law, or Theorem 2.

Proof and Lean reading notes

Proof idea: Use the compiled equality of every inclusive prefix. For an arbitrary finite coordinate set, select it from a containing prefix, push both prefix laws through that selector, and then apply Mathlib's projective-limit uniqueness theorem to the resulting common family of finite-dimensional laws.
Lean reading notes: The canary reports only propext, Classical.choice, and Quot.sound. Full-law equality does not justify conditioning on occurrence of random pull times or totalizing missing pulls; those remain separate obligations.
Teaching dependencies: BanditRLProof.Thompson.latentArmStreamVisibleTrajectoryMeasure_map_frestrictLe_eq_native, BanditRLProof.Thompson.nativeStationaryTrajectoryMeasure, BanditRLProof.Thompson.latentArmStreamVisiblePrefixNextPair_eq_compProd

Exact Lean statement

theorem latentArmStreamVisibleTrajectoryMeasure_eq_native {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : (latentArmStreamTrajectoryMeasure algorithm env nu).map Prod.snd = nativeStationaryTrajectoryMeasure algorithm nu

Open in the declaration catalog Open source at line 356

Mathematics ↔ Lean

On the source-shaped generated two-arm SGB process, every finite block of…

Lean declarationBanditRLProof.StochasticGradientBandit.twoArmFixedIIDTrajectoryMeasure_map_optimalPullTimeRewardBlock_eq_latentMasked

Compiled

Plain-English statement. On the source-shaped generated two-arm SGB process, every finite block of optimal-arm pull times and observed rewards has exactly the law of a missing-pull-aware block on the latent coupling.

Mathematical reading. Formula renderer unavailable; readable fallback: On the source-shaped generated two-arm SGB process, every finite block of optimal-arm pull times and observed rewards has exactly the law of a missing-pull-aware block on the latent coupling.\(\mathcal L((\tau_i,Y_{\tau_i})_{i<m})=\mathcal L((\tau_i,\widetilde Y_i^{\mathrm{mask}})_{i<m}).\)

Intuition: When the ith optimal-arm pull occurs, its reward is the ith coordinate of the pre-sampled optimal-arm stream. If that pull never occurs, the theorem keeps the missing time and the stopped fallback visible instead of silently inventing an IID observation.
Why it is needed: This is the first source-facing finite selected-block transport after complete visible/native law equality. Its explicit dependence boundary is consumed by the downstream Appendix-C phase-event and probability-split layers.
Place in the proof: The first eight declarations in this compiled selected-block module establish the masked coupling law; fourteen downstream declarations transport the exact finite phase event and ten more split its pure probability into all-present and missing-pull branches. None is an unmasked product or selected-IID theorem. Future/no-return, ballot probability, asymptotic assembly, and Theorem 2 remain open.

Proof and Lean reading notes

Proof idea: Package each pull time with its stopped reward, use the almost-sure nth-pull latent-coordinate readout at every finite block coordinate, transport the block through complete visible/native trajectory-law equality, and normalize the Unit-environment source trajectory to the native stationary process.
Lean reading notes: The `WithTop Nat` time coordinate keeps missing pulls explicit. The canary checks the eight block-transport declarations plus the fourteen phase-event declarations and prints only the baseline axioms propext, Classical.choice, and Quot.sound for the transport endpoints.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullReward_eq_latentCoordinate_ae, BanditRLProof.Thompson.latentArmStreamVisibleTrajectoryMeasure_eq_native, BanditRLProof.StochasticGradientBandit.twoArmFixedIIDLatentTrajectoryMeasure_map_optimalPrefix_eq_pi

Exact Lean statement

theorem twoArmFixedIIDTrajectoryMeasure_map_optimalPullTimeRewardBlock_eq_latentMasked (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) (m : Nat) : Measure.map (twoArmOptimalPullTimeRewardBlock (Env := Unit) m) (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) = Measure.map (twoArmLatentMaskedOptimalPullBlock m) (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta)

Open in the declaration catalog Open source at line 335

Mathematics ↔ Lean

The source-generated finite Appendix-C S0/S1 event has exactly the same…

Lean declarationBanditRLProof.StochasticGradientBandit.twoArmFixedIIDTrajectoryMeasure_appendixCGeneratedPhaseEvent_eq_latent

Compiled

Plain-English statement. The source-generated finite Appendix-C S0/S1 event has exactly the same probability as the latent optimal-arm reward pattern intersected with the event that every requested pull occurs.

Mathematical reading. Formula renderer unavailable; readable fallback: The source-generated finite Appendix-C S0/S1 event has exactly the same probability as the latent optimal-arm reward pattern intersected with the event that every requested pull occurs.\(\mathbb P_{\mathrm{src}}(E^{\mathrm{phase}}_{n_0,n_1,s})=\mathbb P_{\mathrm{latent}}(E^{\mathrm{rewards}}_{n_0,n_1,s}\cap E^{\mathrm{occur}}_{n_0+n_1}).\)

Intuition: S0 requires an initial block of minus-one rewards. S1 restricts rewards to plus or minus one, fixes the terminal sum, and keeps every running prefix sum nonpositive. The all-pulls-present event stays visible because it depends on the adaptive trajectory.
Why it is needed: This is the first exact transport of the paper's finite Appendix-C phase event. It advances the source proof while avoiding the invalid shortcut of treating adaptively selected rewards as IID after conditioning on occurrence.
Place in the proof: This terminal closes a fourteen-declaration compiled phase-event layer. A downstream ten-declaration layer now gives its exact missing/all-present probability split, but no selected-IID law, positive lower bound, future/no-return statement, ballot asymptotic, or Theorem 2.

Proof and Lean reading notes

Proof idea: Define measurable reward, occurrence, observed, latent, and generated events; prove that the masked readout equals the latent arm-zero prefix on the all-pulls-present boundary; then apply the compiled source-to-masked-block pushforward equality.
Lean reading notes: The exact S1 terminal sum is an explicit `phaseOneTotal` parameter for a later rounded-Rademacher layer. The canary reports only propext, Classical.choice, and Quot.sound for this terminal.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.twoArmFixedIIDTrajectoryMeasure_map_optimalPullTimeRewardBlock_eq_latentMasked, BanditRLProof.StochasticGradientBandit.twoArmLatentMaskedOptimalPullBlock_preimage_appendixCObservedPhaseEvent, BanditRLProof.StochasticGradientBandit.measurableSet_twoArmAppendixCObservedPhaseEvent

Exact Lean statement

theorem twoArmFixedIIDTrajectoryMeasure_appendixCGeneratedPhaseEvent_eq_latent (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) (n0 n1 : Nat) (phaseOneTotal : Real) : (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) (twoArmAppendixCGeneratedPhaseEvent n0 n1 phaseOneTotal) = (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta) (twoArmAppendixCLatentPhaseEvent n0 n1 phaseOneTotal)

Open in the declaration catalog Open source at line 610

Mathematics ↔ Lean

The pure latent Appendix-C reward-pattern probability is exactly the sum of…

Lean declarationBanditRLProof.StochasticGradientBandit.twoArmAppendixCRewardPhaseProbability_eq_generated_add_missing

Compiled

Plain-English statement. The pure latent Appendix-C reward-pattern probability is exactly the sum of the generated all-pulls-present phase probability and an explicit missing-pull phase probability.

Mathematical reading. Formula renderer unavailable; readable fallback: The pure latent Appendix-C reward-pattern probability is exactly the sum of the generated all-pulls-present phase probability and an explicit missing-pull phase probability.\(\mathbb P(E^{\mathrm{pure}})=\mathbb P(E^{\mathrm{generated}})+\mathbb P(E^{\mathrm{missing}}).\)

Intuition: Every latent reward block with the required S0/S1 pattern falls into exactly one of two cases: all requested optimal-arm pulls occur, or at least one requested pull time is top. The first case is already transported to the generated process; the second stays explicit.
Why it is needed: This closes the finite missing-pull/all-present probability decomposition without conditioning on occurrence or pretending that adaptive stopped rewards are IID.
Place in the proof: This terminal closes a ten-declaration compiled dichotomy layer. A downstream four-declaration route now maps the missing branch into a terminal-count-below event, transports its mass, and charges that existing mass against finite-horizon expected regret. It does not provide the generated all-present phase trigger, a positive phase probability, the future/no-return law, the ballot estimate, or Theorem 2.

Proof and Lean reading notes

Proof idea: Define the pure and missing latent events, prove the pure event is the disjoint union of the occurrence-intersected event and the missing event, evaluate the pure event under the finite arm-zero product law, and substitute the compiled source phase-event transport.
Lean reading notes: Missing-pull membership exposes a concrete coordinate whose nth-pull time is `WithTop.top`. The terminal canary reports only propext, Classical.choice, and Quot.sound.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.twoArmAppendixCPureLatentRewardEvent_eq_union_phase_missing, BanditRLProof.StochasticGradientBandit.disjoint_twoArmAppendixCLatentPhaseEvent_missing, BanditRLProof.StochasticGradientBandit.twoArmFixedIIDTrajectoryMeasure_appendixCGeneratedPhaseEvent_eq_latent

Exact Lean statement

theorem twoArmAppendixCRewardPhaseProbability_eq_generated_add_missing (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta : Real) (n0 n1 : Nat) (phaseOneTotal : Real) : (Measure.pi (fun _ : Fin (n0 + n1) => armLaw 0) : Measure (Fin (n0 + n1) -> Real)) (twoArmAppendixCRewardPhaseEvent n0 n1 phaseOneTotal) = (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) (twoArmAppendixCGeneratedPhaseEvent n0 n1 phaseOneTotal) + (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta) (twoArmAppendixCMissingPullLatentPhaseEvent n0 n1 phaseOneTotal)

Open in the declaration catalog Open source at line 925

Mathematics ↔ Lean

If one of the requested optimal-arm pulls in the finite Appendix-C block…

Lean declarationBanditRLProof.StochasticGradientBandit.twoArmAppendixCMissingPullLatentPhaseEvent_subset_terminalCountBelow

Compiled

Plain-English statement. If one of the requested optimal-arm pulls in the finite Appendix-C block never occurs, then at every finite horizon the optimal arm has been pulled fewer times than the requested block length.

Mathematical reading. Formula renderer unavailable; readable fallback: If one of the requested optimal-arm pulls in the finite Appendix-C block never occurs, then at every finite horizon the optimal arm has been pulled fewer times than the requested block length.\(E_m^{\mathrm{missing}}\subseteq\{\omega:N_0(T,\omega)<m\}\quad\text{for every finite }T.\)

Intuition: A missing ith pull is represented by the actual value `WithTop.top`. If the count had already reached i+1 by any finite horizon, the compiled nth-pull specification would produce a finite occurrence time, contradicting that value.
Why it is needed: This turns the previously isolated missing-pull probability branch into a concrete measurable low-count event. A downstream compiled consumer now charges its existing mass against expected regret without inventing a stopped reward or an IID premise.
Place in the proof: This is a compiled deterministic interface, not the generated all-present phase trigger and not a positive probability bound. The future/no-return law, ballot estimate, asymptotic assembly, and Theorem 2 remain open.

Proof and Lean reading notes

Proof idea: Use the top-time characterization to exclude the requested successor count at every horizon, strengthen the bound for a `Fin m` witness, and map missing-event membership into the measurable below-m terminal-count event.
Lean reading notes: The theorem keeps `WithTop.top` as the explicit no-occurrence value. Its canary reports only propext, Classical.choice, and Quot.sound. It proves neither selected-reward IID nor any lower bound on the missing branch's probability.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.mem_twoArmAppendixCMissingPullLatentPhaseEvent_iff, BanditRLProof.StochasticGradientBandit.twoArmOptimalPullCount_lt_of_fin_nthOptimalPullTime_eq_top, BanditRLProof.StochasticGradientBandit.twoArmOptimalPullCountBelowEvent

Exact Lean statement

theorem twoArmAppendixCMissingPullLatentPhaseEvent_subset_terminalCountBelow (n0 n1 : Nat) (phaseOneTotal : Real) (horizon : Nat) : twoArmAppendixCMissingPullLatentPhaseEvent n0 n1 phaseOneTotal ⊆ (fun sample : UCB.ArmRewardStream 2 × ((t : Nat) -> Fin 2 × Real) => ((), sample.2)) ⁻¹' twoArmOptimalPullCountBelowEvent (Env := Unit) (n0 + n1) horizon

Open in the declaration catalog Open source at line 716

Mathematics ↔ Lean

The existing latent missing-pull phase mass is charged against…

Lean declarationBanditRLProof.StochasticGradientBandit.twoArmFixedIIDMissingPullLatentPhase_charge_mul_probability_le_integral

Compiled

Plain-English statement. The existing latent missing-pull phase mass is charged against finite-horizon expected sampled pseudo-regret on the actual generated fixed-IID trajectory.

Mathematical reading. Formula renderer unavailable; readable fallback: The existing latent missing-pull phase mass is charged against finite-horizon expected sampled pseudo-regret on the actual generated fixed-IID trajectory.\(\Delta\bigl(T-(n_0+n_1)\bigr)\,\mathbb P_{\mathrm{latent}}(E^{\mathrm{missing}})\le \mathbb E_{\mathrm{generated}}[R_T^{\mathrm{sampled}}].\)

Intuition: A missing requested pull forces the optimal-arm count below the requested block length at every finite horizon. Exact visible-marginal transport moves that low-count probability to the generated trajectory, where the generic low-count lemma integrates the conservative regret charge.
Why it is needed: This closes the finite-horizon consumer for the missing branch while keeping the genuinely probabilistic source trigger and positive-mass arguments visible as separate obligations.
Place in the proof: This is a compiled finite-horizon consumer. It supplies no positive missing-branch mass, generated all-present phase trigger, selected-IID theorem, future/no-return probability, ballot estimate, asymptotic assembly, or Theorem 2.

Proof and Lean reading notes

Proof idea: Use missing-pull inclusion to obtain a low-count event, transport its probability through the exact latent-visible/generated trajectory marginal, multiply by the nonnegative horizon-minus-block-size charge, and apply the generic low-count expected-regret consumer.
Lean reading notes: The probability on the left is measured on the latent coupling, while the integral on the right is over the source-generated fixed-IID trajectory. The exact marginal theorem and measurable event transport justify that change of measure; the theorem assumes only a nonnegative gap for this deterministic charge.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.twoArmAppendixCMissingPullLatentPhaseEvent_subset_terminalCountBelow, BanditRLProof.StochasticGradientBandit.twoArmFixedIIDLatentTrajectoryMeasure_map_visible_eq_generated, BanditRLProof.StochasticGradientBandit.twoArmFixedIIDMissingPullLatentPhase_probability_le_countBelow, BanditRLProof.StochasticGradientBandit.twoArmOptimalPullCountBelowEvent_charge_mul_probability_le_integral

Exact Lean statement

theorem twoArmFixedIIDMissingPullLatentPhase_charge_mul_probability_le_integral (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta Delta : Real) (hDelta : 0 ≤ Delta) (n0 n1 : Nat) (phaseOneTotal : Real) (horizon : Nat) : Delta * ((horizon - (n0 + n1) : Nat) : Real) * (twoArmFixedIIDLatentTrajectoryMeasure armLaw hprob eta).real (twoArmAppendixCMissingPullLatentPhaseEvent n0 n1 phaseOneTotal) ≤ integral (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) (twoArmSampledPseudoRegret (Env := Unit) Delta horizon)

Open in the declaration catalog Open source at line 791

Mathematics ↔ Lean

On the canonical generated fixed-IID trajectory, the exact regret charge of…

Lean declarationBanditRLProof.StochasticGradientBandit.twoArmFixedIIDStepOneStarvationEvent_charge_mul_probability_le_integral

Compiled

Plain-English statement. On the canonical generated fixed-IID trajectory, the exact regret charge of a measurable fixed-cutoff starvation event times its probability is no larger than expected sampled pseudo-regret.

Mathematical reading. Formula renderer unavailable; readable fallback: On the canonical generated fixed-IID trajectory, the exact regret charge of a measurable fixed-cutoff starvation event times its probability is no larger than expected sampled pseudo-regret.\(\Delta(T-n)\,\mathbb P(E_{c,n,T}^{\mathrm{starve}})\le\mathbb E R_T^{\mathrm{sampled}}.\)

Intuition: If only n optimal-arm pulls occur by horizon T, every other round pulls the suboptimal arm and contributes Delta. Integrating that exact pathwise identity over the starvation event turns event probability into a regret lower bound.
Why it is needed: This isolates the deterministic consumer at Appendix-C Step 1 without hiding the still-missing probability producer behind a theorem-shaped premise.
Place in the proof: This named declaration is a compiled source-shaped consumer, not a partial closure of Theorem 2. The frozen K = 2 terminal remains blocked.

Proof and Lean reading notes

Proof idea: Make the trigger and final-count event measurable, identify two-arm sampled regret with Delta times suboptimal pulls, prove the exact Delta(T-n) charge on the event, and compare the integral of its indicator with total expected regret.
Lean reading notes: The event uses an externally fixed chronological cutoff. Separate compiled modules construct the random nth-pull stopping prefix, prove the latent fixed-arm product/readout layer, establish deterministic-time freshness and complete visible/native trajectory-law equality, transport finite pull-time/reward blocks and the exact finite S0/S1 phase event, split its pure probability into all-present and missing-pull branches, and charge the missing branch against finite-horizon expected regret. The generated all-present phase still lacks its source fixed-cutoff trigger. No module yet proves positive missing mass, conditional no-return probability >= 1/2, the Rademacher/binomial ballot probability, or the polynomial asymptotic lower bound.
Teaching dependencies: BanditRLProof.StochasticGradientBandit.twoArmStepOneStarvationEvent_charge_mul_probability_le_integral, BanditRLProof.StochasticGradientBandit.measurableSet_twoArmStepOneStarvationEvent, BanditRLProof.StochasticGradientBandit.twoArmStepOneStarvationEvent_sampledPseudoRegret_eq

Exact Lean statement

theorem twoArmFixedIIDStepOneStarvationEvent_charge_mul_probability_le_integral (armLaw : Fin 2 -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (eta Delta : Real) (hDelta : 0 <= Delta) (cutoff n horizon : Nat) : Delta * ((horizon - n : Nat) : Real) * (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)).real (twoArmStepOneStarvationEvent (Env := Unit) eta cutoff n horizon) <= integral (twoArmTrajectoryMeasure (Measure.dirac ()) eta (twoArmFixedIIDEnvironment armLaw hprob)) (twoArmSampledPseudoRegret (Env := Unit) Delta horizon)

Open in the declaration catalog Open source at line 451

Chapter implementation status

The compact summary keeps the reading route visible. Open it for source-linked declarations and exact remaining gaps.

Open 21 implementation records13 compiled · 5 partial · 2 blocked · 1 planned

Milestone	Status	Lean declaration	Remaining gap
Direct LeanMachineLearning toolchain identity	Blocked	No local declaration yet	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.
Budget-exhaustion stopping time	Compiled	`BanditRLProof.Budget.isStoppingTime_budgetExhaustionTime_of_adapted`	—
Bandits-with-knapsacks regret theorem	Blocked	`BanditRLProof.Budget.isStoppingTime_budgetExhaustionTime_of_adapted`	Resource-consumption and feasibility model. Primal-dual comparison. Final resource-constrained regret assembly.
Source-faithful delayed-feedback accounting	Compiled	`BanditRLProof.DelayedFeedback.observedBeforeBanditRLProof.DelayedFeedback.outstandingAtBanditRLProof.DelayedFeedback.observedBefore_disjoint_outstandingAt` Open 14 more declarations `BanditRLProof.DelayedFeedback.observedBefore_union_outstandingAtBanditRLProof.DelayedFeedback.card_observedBefore_add_card_outstandingAtBanditRLProof.DelayedFeedback.outstandingCountBanditRLProof.DelayedFeedback.maxOutstandingBeforeThroughBanditRLProof.DelayedFeedback.outstandingCount_le_roundBanditRLProof.DelayedFeedback.outstandingCount_le_maxOutstandingBeforeThroughBanditRLProof.DelayedFeedback.oneBasedDelayShiftBanditRLProof.DelayedFeedback.paperMissingAtEndBanditRLProof.DelayedFeedback.paperMissingAtEnd_eq_outstandingAt_oneBasedDelayShiftBanditRLProof.DelayedFeedback.paperMissingCountBanditRLProof.DelayedFeedback.paperMissingCount_eq_outstandingCount_oneBasedDelayShiftBanditRLProof.DelayedFeedback.paperMissingCount_le_roundBanditRLProof.DelayedFeedback.paperSigmaMaxThroughBanditRLProof.DelayedFeedback.paperMissingCount_le_paperSigmaMaxThrough`	—
Causal action-time view and new-feedback processing	Compiled	`BanditRLProof.DelayedFeedback.ActionTimeViewBanditRLProof.DelayedFeedback.ActionTimeView.extBanditRLProof.DelayedFeedback.actionTimeViewAt` Open 17 more declarations `BanditRLProof.DelayedFeedback.CausalDecisionRuleBanditRLProof.DelayedFeedback.actionTimeViewAt_pastAction_of_ltBanditRLProof.DelayedFeedback.actionTimeViewAt_pastAction_of_not_ltBanditRLProof.DelayedFeedback.actionTimeViewAt_observedLoss_of_memBanditRLProof.DelayedFeedback.actionTimeViewAt_observedLoss_of_not_memBanditRLProof.DelayedFeedback.actionTimeViewAt_outstanding_loss_hiddenBanditRLProof.DelayedFeedback.actionTimeViewAt_eq_of_observation_equivalentBanditRLProof.DelayedFeedback.causalDecision_eq_of_observation_equivalentBanditRLProof.DelayedFeedback.newlyObservedBeforeBanditRLProof.DelayedFeedback.observedBefore_monoBanditRLProof.DelayedFeedback.processed_disjoint_newlyObservedBeforeBanditRLProof.DelayedFeedback.processed_union_newlyObservedBeforeBanditRLProof.DelayedFeedback.processAllNewBanditRLProof.DelayedFeedback.processAllNew_eq_observedBeforeBanditRLProof.DelayedFeedback.previousObservedBefore_subset_currentBanditRLProof.DelayedFeedback.processAllNew_from_previous_eq_currentBanditRLProof.DelayedFeedback.outstandingAt_disjoint_newlyObservedBefore`	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.
Delayed SAPO active-arm allocation leaf	Compiled	`BanditRLProof.DelayedFeedback.inactiveArmsBanditRLProof.DelayedFeedback.activeEqualShareBanditRLProof.DelayedFeedback.delayedSAPOProbability` Open 5 more declarations `BanditRLProof.DelayedFeedback.delayedSAPOProbability_of_activeBanditRLProof.DelayedFeedback.delayedSAPOProbability_of_inactiveBanditRLProof.DelayedFeedback.activeEqualShare_nonnegBanditRLProof.DelayedFeedback.delayedSAPOProbability_nonnegBanditRLProof.DelayedFeedback.sum_delayedSAPOProbability_eq_one`	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.
Optimal-arm survival and causal one-round action law	Compiled	`BanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshotBanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.eliminatedBanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.remainingActive` Open 16 more declarations `BanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.mem_eliminated_iffBanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.mem_remainingActive_iffBanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.OptimalArmSurvivalCertificateBanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.optimal_mem_remainingActive_of_certificateBanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.remainingActive_nonempty_of_certificateBanditRLProof.DelayedFeedback.DelayedSAPOEliminationSnapshot.sum_delayedSAPOProbability_after_elimination_eq_oneBanditRLProof.DelayedFeedback.DelayedSAPOAllocationBanditRLProof.DelayedFeedback.DelayedSAPOAllocation.probabilityBanditRLProof.DelayedFeedback.DelayedSAPOAllocation.probability_nonnegativeBanditRLProof.DelayedFeedback.DelayedSAPOAllocation.sum_probability_eq_oneBanditRLProof.DelayedFeedback.DelayedSAPOAllocation.finiteActionDistributionBanditRLProof.DelayedFeedback.DelayedSAPOAllocation.actionMeasureBanditRLProof.DelayedFeedback.DelayedSAPOAllocation.actionMeasure_isProbabilityMeasureBanditRLProof.DelayedFeedback.causalDelayedSAPOActionMeasureRuleBanditRLProof.DelayedFeedback.causalDelayedSAPOActionMeasureRule_isProbabilityMeasureBanditRLProof.DelayedFeedback.causalDelayedSAPOActionMeasureRule_eq_of_observation_equivalent`	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.
Source-shaped good-event projection for optimal-arm survival	Compiled	`BanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshotBanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.sourceUcbStarBanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.EliminationGoodEvent` Open 8 more declarations `BanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.optimalMean_le_ucbStar_of_eliminationGoodEventBanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.optimalArmSurvivalCertificate_of_eliminationGoodEventBanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.optimal_mem_remainingActive_of_eliminationGoodEventBanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.eliminationGoodEventSetBanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.optimalSurvivalEventSetBanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.eliminationGoodEventSet_subset_optimalSurvivalEventSetBanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.measure_optimalSurvivalEventSet_compl_leBanditRLProof.DelayedFeedback.DelayedSAPOSourceConfidenceSnapshot.measure_optimalSurvivalEventSet_compl_le_of_goodEvent`	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.
Corollary-D.8 union assembly to D.9 survival	Compiled	`BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventComponentBanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamilyBanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.componentFailure` Open 11 more declarations `BanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.failureSetBanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.sourceGoodEventSetBanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.sourceGoodEventSet_complBanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.measure_sourceGoodEventSet_compl_le_sumBanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.linearFailureBudgetBanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.doubleLinearFailureBudgetBanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.sourceComponentFailureBudgetBanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.sum_sourceComponentFailureBudget_eq_nine_divBanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.measure_sourceGoodEventSet_compl_le_nine_divBanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.measure_eliminationGoodEventSet_compl_le_nine_divBanditRLProof.DelayedFeedback.DelayedSAPOGoodEventFailureFamily.measure_optimalSurvivalEventSet_compl_le_nine_div`	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.
Lemma-D.10/D.12 width-direction diagnostic and conditional same-snapshot skeleton	Partial	`BanditRLProof.DelayedFeedback.sourceEmpiricalWidthScaleBanditRLProof.DelayedFeedback.sourceEmpiricalWidthScale_antitoneBanditRLProof.DelayedFeedback.one_le_ten_mul_sourceEmpiricalWidthScale_of_count_le_96_mul_scale` Open 16 more declarations `BanditRLProof.DelayedFeedback.one_le_ten_mul_sourceEmpiricalWidthScale_two_log_of_small_countBanditRLProof.DelayedFeedback.sourceEmpiricalWidthScale_one_oneBanditRLProof.DelayedFeedback.sourceEmpiricalWidthScale_one_fourBanditRLProof.DelayedFeedback.not_sourceEmpiricalWidthScale_one_le_fourBanditRLProof.DelayedFeedback.not_sourceEmpiricalWidthScale_horizon_four_one_le_fourBanditRLProof.DelayedFeedback.eight_mul_empiricalWidth_lt_gap_of_mem_eliminatedBanditRLProof.DelayedFeedback.gap_le_sixteen_mul_empiricalWidth_of_mem_remainingActiveBanditRLProof.DelayedFeedback.gap_le_sixteen_mul_empiricalWidth_of_mem_remainingActive_of_large_or_small_countBanditRLProof.DelayedFeedback.gap_le_twenty_mul_gap_at_earlier_elimination_snapshotBanditRLProof.DelayedFeedback.gap_le_twenty_mul_gap_at_earlier_elimination_snapshot_of_large_or_small_countBanditRLProof.DelayedFeedback.DelayedSAPOD10D12GapOrderingContractBanditRLProof.DelayedFeedback.DelayedSAPOD10D12GapOrderingContract.surrogateGapBanditRLProof.DelayedFeedback.DelayedSAPOD10D12GapOrderingContract.surrogateGap_le_gapBanditRLProof.DelayedFeedback.DelayedSAPOD10D12GapOrderingContract.gap_le_two_mul_surrogateGapBanditRLProof.DelayedFeedback.DelayedSAPOD10D12GapOrderingContract.d12_gap_ordering_chainBanditRLProof.DelayedFeedback.DelayedSAPOD10D12GapOrderingContract.gap_le_twenty_mul_gap_of_eliminationPrefixIndex_le`	A measurable generated Delayed-SAPO trajectory, its Algorithm-5 transition-and-invariant-to-summary producer, and the D.4 simultaneous probability producer for the two count inequalities consumed by the compiled trace-summary adapter. 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.
Definition-D.1 active-count to same-prefix width producer	Compiled	`BanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefixBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefix.processedPullCountBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefix.expectedPullMass` Open 13 more declarations `BanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefix.expectedPullMass_eq_of_active_throughoutBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefixCountCertificateBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefixCountCertificate.sourceEmpiricalWidthScale_nonnegBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefixCountCertificate.sourceEmpiricalWidthScale_le_oneBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefixCountCertificate.sourceEmpiricalWidthScale_le_three_of_count_le_eight_mulBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefixCountCertificate.expectedPullMass_eq_of_mem_activeBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefixCountCertificate.quarter_count_sub_six_log_le_count_of_mem_activeBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefixCountCertificate.eighth_count_le_count_of_large_countBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefixCountCertificate.empiricalWidth_le_three_of_large_countBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefixCountCertificate.empiricalWidth_le_ten_of_mem_activeBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefixCountCertificate.ucbStar_le_empiricalMean_add_widthBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefixCountCertificate.activeArmGapBranchBanditRLProof.DelayedFeedback.DelayedSAPOProcessedPrefixCountCertificate.gap_le_twenty_mul_gap_at_earlier_elimination_snapshot_of_countCertificate`	A measurable randomized Algorithm-5 trajectory and numerical BSC/EAP transition that supplies the explicit fields consumed by the compiled structural processing step. Lemma D.4's simultaneous probability bound for the D.1 count clause on the generated trajectory. An ordered elimination-snapshot wrapper and the remaining D.13–D.21 regret chain.
Processed trace summary to source-time ledger	Compiled	`BanditRLProof.DelayedFeedback.DelayedSAPOProcessedTraceSummaryBanditRLProof.DelayedFeedback.DelayedSAPOProcessedTraceSummary.toProcessedPrefixBanditRLProof.DelayedFeedback.DelayedSAPOProcessedTraceSummary.empiricalWidthAt` Open 6 more declarations `BanditRLProof.DelayedFeedback.DelayedSAPOProcessedTraceSummary.empiricalUpperAtBanditRLProof.DelayedFeedback.DelayedSAPOProcessedTraceSummary.toConfidenceSnapshotBanditRLProof.DelayedFeedback.DelayedSAPOProcessedTraceSummary.D4CountClauseBanditRLProof.DelayedFeedback.DelayedSAPOProcessedTraceSummary.currentActive_subset_activeAt_sourceIndexBanditRLProof.DelayedFeedback.DelayedSAPOProcessedTraceSummary.toProcessedPrefixCountCertificateBanditRLProof.DelayedFeedback.DelayedSAPOProcessedTraceSummary.gap_le_twenty_mul_gap_at_earlier_elimination_snapshot_of_traceSummary`	A measurable causal randomized Delayed-SAPO kernel and numerical BSC/EAP transition that supply the explicit round state and confidence surfaces consumed by the compiled structural processing step. Lemma D.4's simultaneous 2/T probability bound for the two count inequalities over the source's processed-prefix family. The switch branch, an unconditional generated-trajectory D.12 / main-text Lemma 4.2 theorem, and the remaining source regret chain.
One ordered no-switch Algorithm-5 processing step	Compiled	`BanditRLProof.DelayedFeedback.DelayedSAPOStructuralRoundStateBanditRLProof.DelayedFeedback.DelayedSAPOStructuralRoundState.source_le_roundStartBanditRLProof.DelayedFeedback.DelayedSAPOStructuralRoundState.currentActive_subset_activeAtSourceRound` Open 12 more declarations `BanditRLProof.DelayedFeedback.DelayedSAPONoSwitchProcessOneBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchProcessOne.extendedOrderBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchProcessOne.sourceRound_not_memBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchProcessOne.extendedOrder_nodupBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchProcessOne.extendedOrder_availableBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchProcessOne.extendedSource_le_roundStartBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchProcessOne.currentActive_subset_extendedSourceActiveBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchProcessOne.toPreEliminationSummaryBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchProcessOne.line8RemainingActive_subset_currentActiveBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchProcessOne.afterLine8BanditRLProof.DelayedFeedback.DelayedSAPONoSwitchProcessOne.afterLine8_currentActive_subset_beforeBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchProcessOne.afterLine8_preserves_roundStart`	The numerical BSC/EAP update that constructs the empirical and importance-weighted confidence surfaces read by this structural step. Round finalization, the switch branch, and a measurable randomized recursive Delayed-SAPO trajectory. Lemma D.4's simultaneous probability bound, the generated-trajectory version of the multi-snapshot elimination argument, and every paper regret endpoint.
Ordered no-switch trace closes the temporal elimination premise	Compiled	`BanditRLProof.DelayedFeedback.DelayedSAPONoSwitchRoundCloseBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchRoundClose.processedOrder_toFinset_eq_observedBeforeBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchRoundClose.nextRoundState` Open 9 more declarations `BanditRLProof.DelayedFeedback.DelayedSAPONoSwitchRoundClose.nextRoundState_currentActionRoundBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchRoundClose.nextRoundState_processedOrderBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchRoundClose.nextRoundState_currentActiveBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchStructuralStepBanditRLProof.DelayedFeedback.DelayedSAPONoSwitchStructuralReachableBanditRLProof.DelayedFeedback.currentActive_subset_of_structuralStepBanditRLProof.DelayedFeedback.currentActive_subset_of_structuralReachableBanditRLProof.DelayedFeedback.mem_earlierRemainingActive_of_laterEliminatedBanditRLProof.DelayedFeedback.gap_le_twenty_mul_gap_of_ordered_no_switch_eliminations`	Numerical BSC/EAP production and a measurable randomized Delayed-SAPO trajectory that generate the structural states and confidence surfaces. Lemma D.4's simultaneous 2/T probability bound and the Definition-D.1 good-event producer. The switch branch, an unconditional source Lemma D.12 / main-text Lemma 4.2 theorem, and both regret endpoints.
Appendix D.11 nonnegative-gap half-set core	Compiled	`BanditRLProof.DelayedFeedback.finiteAverageGapBanditRLProof.DelayedFeedback.aboveTwiceAverageGapBanditRLProof.DelayedFeedback.two_mul_card_aboveTwiceAverageGap_le` Open 3 more declarations `BanditRLProof.DelayedFeedback.sourceStochasticLossGapBanditRLProof.DelayedFeedback.sourceStochasticLossGap_nonnegBanditRLProof.DelayedFeedback.two_mul_card_sourceStochasticLossGap_aboveTwiceAverage_le`	A source-faithful Lemma D.13 statement resolving the printed witness/index mismatch and half-active-set convention. The generated stochastic Delayed-SAPO process and its regret endpoint.
Algorithm 5 line-10 eliminated-arm initialization	Compiled	`BanditRLProof.DelayedFeedback.delayedSAPOInitialEliminatedProbabilityBanditRLProof.DelayedFeedback.delayedSAPOInitialPhaseTargetBanditRLProof.DelayedFeedback.sourceEmpiricalWidthScale_pos` Open 28 more declarations `BanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitializationBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmBankBanditRLProof.DelayedFeedback.ActiveArmsUninitializedBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.ofProcessOneBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.initializeIfEliminatedBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.initializeNewlyEliminatedBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.initializeIfEliminated_eq_some_iffBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.initializeIfEliminated_eq_none_iffBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.initializeNewlyEliminated_of_memBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.initializeNewlyEliminated_of_not_memBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.mem_eliminated_of_initializeNewlyEliminated_ne_priorBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.initializeNewlyEliminated_eq_prior_of_mem_remainingActiveBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.prior_eq_none_of_mem_eliminatedBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.remainingActive_uninitialized_after_initializeBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.ofProcessOne_armBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.ofProcessOne_eliminationRoundBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.ofProcessOne_eliminationProcessedOrderBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.ofProcessOne_errorCountBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.ofProcessOne_phaseIndexBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.ofProcessOne_phaseSamplesBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.ofProcessOne_processedAtProbabilityLevelBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.initialProbability_posBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.initialProbability_le_oneBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.surrogateGap_nonnegBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.surrogateGap_posBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.initialPhaseTarget_nonnegBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.initialPhaseTarget_posBanditRLProof.DelayedFeedback.DelayedSAPOEliminatedArmInitialization.initializeNewlyEliminated_spec_of_mem`	The source EAP phase transition, integer stopping rule, sample/confidence-set evolution, and recursive probability bank. BSC, the measurable generated Delayed-SAPO trajectory, D.4's simultaneous probability theorem, and both regret endpoints.
Source-frozen delayed best-of-both-worlds endpoint audit	Partial	`BanditRLProof.DelayedFeedback.SameAlgorithmMultiRegimeContractBanditRLProof.DelayedFeedback.SameAlgorithmMultiRegimeContract.stochasticClaimBanditRLProof.DelayedFeedback.SameAlgorithmMultiRegimeContract.adversarialClaim` Open 2 more declarations `BanditRLProof.DelayedFeedback.SameAlgorithmMultiRegimeContract.stochasticClaim_iff_shared_fieldsBanditRLProof.DelayedFeedback.SameAlgorithmMultiRegimeContract.adversarialClaim_iff_shared_fields`	The complete Definition-D.1 event, its D.2–D.7 component probability producers, Delayed SAPO BSC/EAP phase transitions beyond the line-10 initializer, 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. A measurable generated-state trajectory and numerical BSC/EAP producer for the structural steps, the D.4 probability proof, a clarification or amendment of the printed D.10 transport, and an unconditional generated-trajectory D.12 / main-text Lemma 4.2 bridge. The stochastic-instance and oblivious-adversarial regret endpoints for the same algorithm identity.
Source-frozen succinct lower-bound geometry audit	Partial	`BanditRLProof.LowerBounds.Succinct.SuccinctUnitSystemBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.sourceQBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.sourceQSet_bddAbove` Open 51 more declarations `BanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.le_sourceQ_of_memBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.sourceQ_le_normBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.sourceQ_nonnegBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.sourceQ_zeroBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.abs_inner_le_sourceQ_of_memBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.sourceQ_eq_zero_of_atom_orthogonalBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.sourceRBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.sourceRSet_not_bddAbove_of_nonzero_atom_orthogonalBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupportBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.correlationSum_le_oneBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.inner_basis_basisBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.maxAbsCoefficientBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.abs_le_maxAbsCoefficientBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.maxAbsCoefficient_nonnegBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.exists_abs_eq_maxAbsCoefficientBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.supportCombinationBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.signedSupportAtomBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.signedSupportAtom_memBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.sourceQ_supportCombination_leBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.inner_supportCombination_basisBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.inner_supportCombination_signedSupportAtomBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.sourceQ_supportCombination_eqBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.coefficientSignBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.abs_coefficientSignBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.coefficientSign_mulBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.supportSignCombinationBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.maxAbsCoefficient_coefficientSignBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.sourceQ_supportSignCombinationBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.inner_supportCombination_supportSignCombinationBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.inner_supportCombination_le_sumAbs_mul_sourceQBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.inner_supportCombination_le_sumAbs_of_sourceQ_le_oneBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.sourceRSet_bddAboveBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.sourceR_supportCombination_eqBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.orthonormalBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.coefficientSign_coefficientSignBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.coefficientSign_mul_selfBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctSupport.norm_sq_supportSignCombinationBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.SuccinctRepresentationBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.StrictSuccinctRepresentationBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsSuccinctAtBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.IsStrictlySuccinctAtBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.SuccinctRepresentation.sourceR_eq_sumAbsBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.SuccinctRepresentation.inner_supportSignCombination_eq_sumAbsBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.SuccinctRepresentation.sourceQ_supportSignCombination_eq_oneBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.SuccinctRepresentation.norm_sq_supportSignCombination_eq_sizeBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.SuccinctRepresentation.sumAbs_eqBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.SuccinctRepresentation.abs_inner_strictBasis_supportSignCombination_eq_oneBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.SuccinctRepresentation.strictSize_leBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.StrictSuccinctRepresentation.abs_coefficient_posBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.succinctSize_ge_strictSizeBanditRLProof.LowerBounds.Succinct.SuccinctUnitSystem.strictlySuccinctSize_unique`	A source-faithful global repair for R: a spanning/nondegeneracy premise, an extended-real codomain, or restriction to the atom-generated span or quotient. A source-faithful use of the repaired global R interface in the global primal/dual statements from Lemmas 3.5–3.6. Assumption 3.7's grouped-support geometry, Theorem 3.8's action/parameter construction, its same-policy history-information chain, and both regret regimes.
Source-frozen stochastic-gradient-bandit Theorem-1 endpoint and Theorem-4 contract audit	Partial	`BanditRLProof.StochasticGradientBandit.softmaxDenominatorBanditRLProof.StochasticGradientBandit.softmaxProbabilityBanditRLProof.StochasticGradientBandit.softmaxDenominator_pos` Open 220 more declarations `BanditRLProof.StochasticGradientBandit.softmaxProbability_posBanditRLProof.StochasticGradientBandit.softmaxProbability_nonnegBanditRLProof.StochasticGradientBandit.softmaxProbability_sumBanditRLProof.StochasticGradientBandit.softmaxProbability_le_oneBanditRLProof.StochasticGradientBandit.sourceIncrementBanditRLProof.StochasticGradientBandit.sourceIncrement_eq_indicatorBanditRLProof.StochasticGradientBandit.sum_sourceIncrementBanditRLProof.StochasticGradientBandit.policyValueBanditRLProof.StochasticGradientBandit.expectedSourceIncrementBanditRLProof.StochasticGradientBandit.expectedSourceIncrement_eq_gradientCoordinateBanditRLProof.StochasticGradientBandit.instantaneousGapBanditRLProof.StochasticGradientBandit.instantaneousGap_eq_bestMean_sub_policyValueBanditRLProof.StochasticGradientBandit.expectedSourceIncrement_eq_gapCoordinateBanditRLProof.StochasticGradientBandit.gapExpectedIncrementBanditRLProof.StochasticGradientBandit.expectedSourceIncrement_eq_gapExpectedIncrementBanditRLProof.StochasticGradientBandit.instantaneousGap_ge_minGap_mul_failureMassBanditRLProof.StochasticGradientBandit.gapExpectedIncrement_best_geBanditRLProof.StochasticGradientBandit.bestParameterIncrementSumBanditRLProof.StochasticGradientBandit.bestParameterIncrementSum_geBanditRLProof.StochasticGradientBandit.sourceExpectedPseudoRegretBanditRLProof.StochasticGradientBandit.instantaneousGap_le_maxGap_mul_failureMassBanditRLProof.StochasticGradientBandit.failureMass_eq_successFailure_add_sqBanditRLProof.StochasticGradientBandit.sourceRegretDecomposition_leBanditRLProof.StochasticGradientBandit.measurable_softmaxProbabilityBanditRLProof.StochasticGradientBandit.measurable_sourceIncrementBanditRLProof.StochasticGradientBandit.historyParameterBanditRLProof.StochasticGradientBandit.historyParameter_zeroBanditRLProof.StochasticGradientBandit.historyParameter_succBanditRLProof.StochasticGradientBandit.measurable_historyParameterBanditRLProof.StochasticGradientBandit.softmaxFiniteActionDistributionBanditRLProof.StochasticGradientBandit.historySoftmaxDistributionSourceBanditRLProof.StochasticGradientBandit.historyAlgorithmBanditRLProof.StochasticGradientBandit.historyAlgorithm_policyBanditRLProof.StochasticGradientBandit.integral_measurableEnvironmentInitialPairKernel_sourceIncrement_eq_expectedSourceIncrementBanditRLProof.StochasticGradientBandit.integral_historyStepKernel_sourceIncrement_eq_expectedSourceIncrementBanditRLProof.StochasticGradientBandit.integral_measurableEnvironmentHistoryStepKernel_sourceIncrement_eq_expectedSourceIncrementBanditRLProof.StochasticGradientBandit.integral_measurableEnvironmentHistoryStepKernel_sourceIncrement_eq_gapCoordinateBanditRLProof.StochasticGradientBandit.trajectoryKernelBanditRLProof.StochasticGradientBandit.trajectoryMeasure_condDistrib_action_zero_given_environmentBanditRLProof.StochasticGradientBandit.trajectoryMeasure_condDistrib_actionBanditRLProof.StochasticGradientBandit.trajectoryMeasure_condDistrib_nextPair_given_environment_prefixBanditRLProof.StochasticGradientBandit.historyParameter_sum_eq_initialBanditRLProof.StochasticGradientBandit.historyParameter_zeroInitialization_sumBanditRLProof.StochasticGradientBandit.twoArmParameterAtBanditRLProof.StochasticGradientBandit.twoArmProbabilityAtBanditRLProof.StochasticGradientBandit.twoArmParameterAt_zeroBanditRLProof.StochasticGradientBandit.twoArmParameterAt_succBanditRLProof.StochasticGradientBandit.twoArmParameterAt_sum_eq_zeroBanditRLProof.StochasticGradientBandit.twoArmParameterAt_one_eq_neg_zeroBanditRLProof.StochasticGradientBandit.twoArmProbabilityAt_zeroBanditRLProof.StochasticGradientBandit.softmaxProbability_one_eq_one_sub_zeroBanditRLProof.StochasticGradientBandit.softmaxProbability_zero_div_oneBanditRLProof.StochasticGradientBandit.finTwo_one_eq_neg_zero_of_sum_eq_zeroBanditRLProof.StochasticGradientBandit.softmaxProbability_zero_div_one_sub_zero_eq_exp_two_mulBanditRLProof.StochasticGradientBandit.exp_two_mul_zero_mul_one_sub_softmaxProbability_zeroBanditRLProof.StochasticGradientBandit.exp_neg_two_mul_zero_mul_softmaxProbability_zeroBanditRLProof.StochasticGradientBandit.twoArmProbabilityAt_exp_two_mul_failure_eq_successBanditRLProof.StochasticGradientBandit.twoArmProbabilityAt_zero_div_failure_eq_exp_two_mulBanditRLProof.StochasticGradientBandit.historyParameter_exp_two_mul_zero_eq_oddsBanditRLProof.StochasticGradientBandit.two_mul_abs_pow_div_factorial_add_two_leBanditRLProof.StochasticGradientBandit.sourceCBanditRLProof.StochasticGradientBandit.sourceC_terms_summableBanditRLProof.StochasticGradientBandit.sourceC_nonnegBanditRLProof.StochasticGradientBandit.sourceC_monoBanditRLProof.StochasticGradientBandit.sourceC_le_exp_two_mulBanditRLProof.StochasticGradientBandit.expTailTwoBanditRLProof.StochasticGradientBandit.expTailTwo_terms_summableBanditRLProof.StochasticGradientBandit.exp_eq_one_add_self_add_expTailTwoBanditRLProof.StochasticGradientBandit.expTailTwo_le_of_abs_leBanditRLProof.StochasticGradientBandit.sq_div_two_mul_sourceC_abs_div_twoBanditRLProof.StochasticGradientBandit.exp_mul_le_sourceEqEightBanditRLProof.StochasticGradientBandit.integral_exp_mul_le_sourceEqEightBanditRLProof.StochasticGradientBandit.integral_exp_mul_le_sourceEqEight_of_ae_abs_le_oneBanditRLProof.StochasticGradientBandit.integral_measurableEnvironmentInitialPairKernel_exp_actionReward_le_sourceEqEight_of_meanBanditRLProof.StochasticGradientBandit.integral_historyStepKernel_exp_actionReward_le_sourceEqEightBanditRLProof.StochasticGradientBandit.integral_historyStepKernel_exp_actionReward_le_sourceEqEight_of_meanBanditRLProof.StochasticGradientBandit.integral_measurableEnvironmentHistoryStepKernel_exp_actionReward_le_sourceEqEight_of_meanBanditRLProof.StochasticGradientBandit.twoArmForwardQBanditRLProof.StochasticGradientBandit.twoArmInverseQBanditRLProof.StochasticGradientBandit.twoArmForwardQ_mul_reward_eq_sourceIncrementBanditRLProof.StochasticGradientBandit.twoArmInverseQ_mul_reward_eq_sourceIncrementBanditRLProof.StochasticGradientBandit.twoArmForwardEqEightRemainder_leBanditRLProof.StochasticGradientBandit.twoArmInverseEqEightRemainder_leBanditRLProof.StochasticGradientBandit.integral_twoArmHistoryStepKernel_exp_forwardSuccessor_leBanditRLProof.StochasticGradientBandit.integral_twoArmHistoryStepKernel_exp_forwardSuccessor_le_add_success_sqBanditRLProof.StochasticGradientBandit.integral_twoArmHistoryStepKernel_exp_inverseSuccessor_leBanditRLProof.StochasticGradientBandit.integral_twoArmHistoryStepKernel_exp_inverseSuccessor_le_sub_failure_sqBanditRLProof.StochasticGradientBandit.softmaxProbability_zeroInitialization_finTwoBanditRLProof.StochasticGradientBandit.integral_twoArmInitialPairKernel_exp_forwardIncrement_leBanditRLProof.StochasticGradientBandit.integral_twoArmInitialPairKernel_exp_inverseIncrement_leBanditRLProof.StochasticGradientBandit.twoArmForwardSuccessorPotentialBanditRLProof.StochasticGradientBandit.twoArmInverseSuccessorPotentialBanditRLProof.StochasticGradientBandit.twoArmForwardRecurrenceBoundBanditRLProof.StochasticGradientBandit.twoArmInverseRecurrenceBoundBanditRLProof.StochasticGradientBandit.measurable_twoArmForwardSuccessorPotentialBanditRLProof.StochasticGradientBandit.measurable_twoArmInverseSuccessorPotentialBanditRLProof.StochasticGradientBandit.measurable_twoArmForwardRecurrenceBoundBanditRLProof.StochasticGradientBandit.measurable_twoArmInverseRecurrenceBoundBanditRLProof.StochasticGradientBandit.TwoArmBoundedFixedMeanEnvironmentContractBanditRLProof.StochasticGradientBandit.integral_measurableTwoArmHistoryStepKernel_forwardSuccessor_leBanditRLProof.StochasticGradientBandit.integral_measurableTwoArmHistoryStepKernel_inverseSuccessor_leBanditRLProof.StochasticGradientBandit.integral_measurableTwoArmHistoryStepKernel_forwardSuccessor_le_of_contractBanditRLProof.StochasticGradientBandit.integral_measurableTwoArmHistoryStepKernel_inverseSuccessor_le_of_contractBanditRLProof.StochasticGradientBandit.twoArmTrajectoryMeasureBanditRLProof.StochasticGradientBandit.twoArmEnvironmentPrefixBanditRLProof.StochasticGradientBandit.twoArmNextPairBanditRLProof.StochasticGradientBandit.measurable_twoArmEnvironmentPrefixBanditRLProof.StochasticGradientBandit.measurable_twoArmNextPairBanditRLProof.StochasticGradientBandit.twoArmPrefixSigmaBanditRLProof.StochasticGradientBandit.twoArmPrefixSigma_monoBanditRLProof.StochasticGradientBandit.twoArmPrefixFiltrationBanditRLProof.StochasticGradientBandit.measurable_twoArmForwardTrajectorySuccessorPotentialBanditRLProof.StochasticGradientBandit.measurable_twoArmInverseTrajectorySuccessorPotentialBanditRLProof.StochasticGradientBandit.trajectoryPrefix_condDistrib_integral_forwardSuccessor_leBanditRLProof.StochasticGradientBandit.trajectoryPrefix_condDistrib_integral_inverseSuccessor_leBanditRLProof.StochasticGradientBandit.integral_twoArmInitialPairKernel_exp_forwardIncrement_le_of_contractBanditRLProof.StochasticGradientBandit.integral_twoArmInitialPairKernel_exp_inverseIncrement_le_of_contractBanditRLProof.StochasticGradientBandit.twoArmTrajectoryMeasure_reward_zero_abs_le_one_aeBanditRLProof.StochasticGradientBandit.twoArmTrajectoryMeasure_reward_succ_abs_le_one_aeBanditRLProof.StochasticGradientBandit.twoArmTrajectoryMeasure_reward_abs_le_one_aeBanditRLProof.StochasticGradientBandit.twoArmTrajectoryMeasure_prefix_rewards_abs_le_one_aeBanditRLProof.StochasticGradientBandit.abs_sourceIncrement_le_abs_reward_of_mem_IccBanditRLProof.StochasticGradientBandit.abs_sourceIncrement_softmax_le_abs_rewardBanditRLProof.StochasticGradientBandit.integrable_measurableTwoArmInitialPairKernel_sourceIncrement_of_contractBanditRLProof.StochasticGradientBandit.integrable_measurableTwoArmHistoryStepKernel_sourceIncrement_of_contractBanditRLProof.StochasticGradientBandit.abs_historyParameter_zeroInitialization_leBanditRLProof.StochasticGradientBandit.twoArmForwardTrajectorySuccessorPotential_eq_exp_historyParameterBanditRLProof.StochasticGradientBandit.twoArmInverseTrajectorySuccessorPotential_eq_exp_historyParameterBanditRLProof.StochasticGradientBandit.integrable_twoArmForwardTrajectorySuccessorPotentialBanditRLProof.StochasticGradientBandit.integrable_twoArmInverseTrajectorySuccessorPotentialBanditRLProof.StochasticGradientBandit.twoArmForwardTrajectorySuccessor_condExp_ae_eq_integral_condDistribBanditRLProof.StochasticGradientBandit.twoArmInverseTrajectorySuccessor_condExp_ae_eq_integral_condDistribBanditRLProof.StochasticGradientBandit.twoArmForwardTrajectorySuccessor_condExp_le_recurrenceBoundBanditRLProof.StochasticGradientBandit.twoArmInverseTrajectorySuccessor_condExp_le_recurrenceBoundBanditRLProof.StochasticGradientBandit.twoArmTrajectoryParameterZeroBanditRLProof.StochasticGradientBandit.twoArmForwardPotentialBanditRLProof.StochasticGradientBandit.twoArmInversePotentialBanditRLProof.StochasticGradientBandit.twoArmSuccessProbabilityBanditRLProof.StochasticGradientBandit.twoArmFailureMassBanditRLProof.StochasticGradientBandit.measurable_twoArmTrajectoryParameterZeroBanditRLProof.StochasticGradientBandit.measurable_twoArmForwardPotentialBanditRLProof.StochasticGradientBandit.measurable_twoArmInversePotentialBanditRLProof.StochasticGradientBandit.measurable_twoArmSuccessProbabilityBanditRLProof.StochasticGradientBandit.measurable_twoArmFailureMassBanditRLProof.StochasticGradientBandit.integrable_twoArmForwardPotentialBanditRLProof.StochasticGradientBandit.integrable_twoArmInversePotentialBanditRLProof.StochasticGradientBandit.integrable_twoArmSuccessProbability_sqBanditRLProof.StochasticGradientBandit.integrable_twoArmFailureMass_sqBanditRLProof.StochasticGradientBandit.twoArmForwardSuccessor_eq_nextPotentialBanditRLProof.StochasticGradientBandit.twoArmInverseSuccessor_eq_nextPotentialBanditRLProof.StochasticGradientBandit.integrable_twoArmForwardRecurrenceBoundBanditRLProof.StochasticGradientBandit.integrable_twoArmInverseRecurrenceBoundBanditRLProof.StochasticGradientBandit.twoArmForwardUnconditionalRecurrenceBanditRLProof.StochasticGradientBandit.twoArmInverseUnconditionalRecurrenceBanditRLProof.StochasticGradientBandit.twoArmScalarForwardIterateBanditRLProof.StochasticGradientBandit.twoArmScalarInverseTelescopeBanditRLProof.StochasticGradientBandit.twoArmForwardFiniteIterationBanditRLProof.StochasticGradientBandit.twoArmInverseFailureMassSqTelescopeBanditRLProof.StochasticGradientBandit.twoArmInverseFailureMassSqSum_le_initial_divBanditRLProof.StochasticGradientBandit.twoArmInitialForwardPotentialBanditRLProof.StochasticGradientBandit.twoArmInitialInversePotentialBanditRLProof.StochasticGradientBandit.measurable_twoArmInitialForwardPotentialBanditRLProof.StochasticGradientBandit.measurable_twoArmInitialInversePotentialBanditRLProof.StochasticGradientBandit.twoArmForwardPotential_zero_eq_initialBanditRLProof.StochasticGradientBandit.twoArmInversePotential_zero_eq_initialBanditRLProof.StochasticGradientBandit.integral_twoArmForwardPotential_zero_kernel_eq_initialBanditRLProof.StochasticGradientBandit.integral_twoArmInversePotential_zero_kernel_eq_initialBanditRLProof.StochasticGradientBandit.twoArmForwardInitialUnconditionalRecurrenceBanditRLProof.StochasticGradientBandit.twoArmInverseInitialUnconditionalRecurrenceBanditRLProof.StochasticGradientBandit.twoArmForwardFiniteIteration_from_source_initialBanditRLProof.StochasticGradientBandit.twoArmFullFailureMassSqSum_leBanditRLProof.StochasticGradientBandit.twoArmFixedIIDRewardKernelBanditRLProof.StochasticGradientBandit.twoArmFixedIIDRewardKernel_applyBanditRLProof.StochasticGradientBandit.twoArmFixedIIDRewardKernel_isMarkovBanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironmentBanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironment_initialFeedback_applyBanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironment_feedback_applyBanditRLProof.StochasticGradientBandit.twoArmFixedIIDReward_aestronglyMeasurableBanditRLProof.StochasticGradientBandit.twoArmFixedIIDEnvironment_contractBanditRLProof.StochasticGradientBandit.integral_twoArmFixedIIDHistoryStepKernel_sourceIncrement_eq_gapCoordinateBanditRLProof.StochasticGradientBandit.twoArmTrajectorySourceIncrementBanditRLProof.StochasticGradientBandit.measurable_twoArmTrajectorySourceIncrementBanditRLProof.StochasticGradientBandit.integrable_twoArmTrajectorySourceIncrementBanditRLProof.StochasticGradientBandit.twoArmTrajectorySourceIncrement_condExp_ae_eq_integral_condDistribBanditRLProof.StochasticGradientBandit.twoArmTrajectorySourceIncrement_condExp_ae_eq_successFailureBanditRLProof.StochasticGradientBandit.twoArmTrajectoryParameterZero_succBanditRLProof.StochasticGradientBandit.integrable_twoArmTrajectoryParameterZeroBanditRLProof.StochasticGradientBandit.integral_twoArmTrajectorySourceIncrement_eq_successFailureBanditRLProof.StochasticGradientBandit.integral_twoArmTrajectoryParameterZero_succBanditRLProof.StochasticGradientBandit.twoArmInitialSourceIncrementBanditRLProof.StochasticGradientBandit.measurable_twoArmInitialSourceIncrementBanditRLProof.StochasticGradientBandit.integral_twoArmInitialSourceIncrement_eq_quarter_gapBanditRLProof.StochasticGradientBandit.integral_twoArmTrajectoryParameterZero_zeroBanditRLProof.StochasticGradientBandit.integral_twoArmTrajectoryParameterZero_eq_successFailureSumBanditRLProof.StochasticGradientBandit.measurable_twoArmSuccessFailureMassBanditRLProof.StochasticGradientBandit.integrable_twoArmSuccessFailureMassBanditRLProof.StochasticGradientBandit.integral_twoArmFailureMass_eq_successFailure_add_sqBanditRLProof.StochasticGradientBandit.twoArmGeneratedExpectedPseudoRegretBanditRLProof.StochasticGradientBandit.twoArmGeneratedExpectedPseudoRegret_eq_parameter_add_failureSqBanditRLProof.StochasticGradientBandit.integral_twoArmTrajectoryParameterZero_le_half_log_forwardPotentialBanditRLProof.StochasticGradientBandit.integral_twoArmSuccessProbability_sq_le_oneBanditRLProof.StochasticGradientBandit.integral_twoArmForwardPotential_le_source_boundBanditRLProof.StochasticGradientBandit.integral_twoArmTrajectoryParameterZero_le_source_log_boundBanditRLProof.StochasticGradientBandit.twoArmActionGapBanditRLProof.StochasticGradientBandit.measurable_twoArmActionGapBanditRLProof.StochasticGradientBandit.integral_twoArmInitialActionGap_eq_halfBanditRLProof.StochasticGradientBandit.integral_twoArmSuccessorActionGap_eq_failureMassBanditRLProof.StochasticGradientBandit.twoArmSampledPseudoRegretBanditRLProof.StochasticGradientBandit.integral_twoArmSampledPseudoRegret_eq_generatedBanditRLProof.StochasticGradientBandit.twoArmGeneratedExpectedPseudoRegret_le_sourceTheoremOneBanditRLProof.StochasticGradientBandit.integral_twoArmSampledPseudoRegret_le_sourceTheoremOneBanditRLProof.StochasticGradientBandit.twoArmFixedIIDDirac_theoremOneBanditRLProof.StochasticGradientBandit.theoremFourStepOneMarginBanditRLProof.StochasticGradientBandit.theoremFourStepFourSurvivalLowerBoundBanditRLProof.StochasticGradientBandit.theoremFourStepOneMargin_posBanditRLProof.StochasticGradientBandit.theoremFourStepFourSurvivalLowerBound_posBanditRLProof.StochasticGradientBandit.theoremFourStepFour_survivalMass_geBanditRLProof.StochasticGradientBandit.theoremFourStepFour_survivalMass_posBanditRLProof.StochasticGradientBandit.theoremFourFiniteGeometricPhaseMass_le_invBanditRLProof.StochasticGradientBandit.theoremFourFiniteTransientMass_le_inv`	The source-faithful two-arm learning-rate regimes and regret endpoints in Theorems 2–3. Theorem 4 still requires the source-faithful general-K generated SGB process, its uniform buffered-event and survival-probability producer, the stopped-supermartingale/Doob route, and the final regret assembly; only the finite source-contract consumers compile. Any broader non-Dirac environment-mixture or non-source extension must remain separate from the exact fixed-IID/Dirac Theorem-1 endpoint.
Prospectively frozen SGB Corollary-1 and Theorem-2 follow-on	Partial	`BanditRLProof.StochasticGradientBandit.twoArmActionGap_le_gapBanditRLProof.StochasticGradientBandit.twoArmSampledPseudoRegret_le_gap_mul_horizonBanditRLProof.StochasticGradientBandit.measurable_twoArmSampledPseudoRegret` Open 135 more declarations `BanditRLProof.StochasticGradientBandit.integrable_twoArmSampledPseudoRegretBanditRLProof.StochasticGradientBandit.integral_twoArmSampledPseudoRegret_le_gap_mul_horizonBanditRLProof.StochasticGradientBandit.corollaryOneEtaBanditRLProof.StochasticGradientBandit.sourceTheoremOne_margin_of_two_mul_eta_sourceC_leBanditRLProof.StochasticGradientBandit.sourceTheoremOne_constant_le_inv_etaBanditRLProof.StochasticGradientBandit.corollaryOneEta_posBanditRLProof.StochasticGradientBandit.corollaryOneEta_sqBanditRLProof.StochasticGradientBandit.corollaryOneEta_le_oneBanditRLProof.StochasticGradientBandit.corollaryOneRateBanditRLProof.StochasticGradientBandit.corollaryOneRate_nonnegBanditRLProof.StochasticGradientBandit.corollaryOneEta_mul_horizon_eq_rateBanditRLProof.StochasticGradientBandit.corollaryOneEta_mul_rate_eq_logBanditRLProof.StochasticGradientBandit.corollaryOne_inv_eta_le_inv_log_two_mul_rateBanditRLProof.StochasticGradientBandit.corollaryOne_log_argument_le_horizon_pow_fourBanditRLProof.StochasticGradientBandit.corollaryOne_log_term_le_two_mul_rateBanditRLProof.StochasticGradientBandit.corollaryOne_gap_mul_horizon_le_exp_constant_mul_rateBanditRLProof.StochasticGradientBandit.corollaryOneAbsoluteConstantBanditRLProof.StochasticGradientBandit.corollaryOne_piecewise_boundBanditRLProof.StochasticGradientBandit.twoArmFixedIIDDirac_corollaryOne_piecewiseBanditRLProof.StochasticGradientBandit.twoArmFixedIIDDirac_corollaryOneBanditRLProof.StochasticGradientBandit.twoArmGeneratedActionBanditRLProof.StochasticGradientBandit.twoArmOptimalPullCountBanditRLProof.StochasticGradientBandit.twoArmStepOneThresholdBanditRLProof.StochasticGradientBandit.twoArmStepOneTriggerEventBanditRLProof.StochasticGradientBandit.twoArmStepOneStarvationEventBanditRLProof.StochasticGradientBandit.measurable_twoArmGeneratedActionBanditRLProof.StochasticGradientBandit.measurable_twoArmOptimalPullCountBanditRLProof.StochasticGradientBandit.measurableSet_twoArmStepOneTriggerEventBanditRLProof.StochasticGradientBandit.measurableSet_twoArmStepOneStarvationEventBanditRLProof.StochasticGradientBandit.twoArmTerminalOptimalPullCountEventBanditRLProof.StochasticGradientBandit.measurableSet_twoArmTerminalOptimalPullCountEventBanditRLProof.StochasticGradientBandit.twoArmOptimalPullCountBelowEventBanditRLProof.StochasticGradientBandit.measurableSet_twoArmOptimalPullCountBelowEventBanditRLProof.StochasticGradientBandit.twoArmOptimalPullCountBelowEvent_eq_iUnion_terminalCountBanditRLProof.StochasticGradientBandit.twoArmTerminalOptimalPullCountEvent_sampledPseudoRegret_eqBanditRLProof.StochasticGradientBandit.twoArmOptimalPullCountBelowEvent_charge_mul_probability_le_integralBanditRLProof.StochasticGradientBandit.twoArmSampledPseudoRegret_nonnegBanditRLProof.StochasticGradientBandit.twoArmSampledPseudoRegret_eq_gap_mul_suboptimalPullCountBanditRLProof.StochasticGradientBandit.twoArmOptimalPullCount_add_suboptimalPullCount_eq_horizonBanditRLProof.StochasticGradientBandit.twoArmSampledPseudoRegret_eq_gap_mul_horizon_sub_of_optimalPullCount_eqBanditRLProof.StochasticGradientBandit.mem_twoArmStepOneStarvationEvent_of_lowProbability_noFurtherOptimalPullBanditRLProof.StochasticGradientBandit.twoArmStepOneStarvationEvent_sampledPseudoRegret_eqBanditRLProof.StochasticGradientBandit.integrable_twoArmSampledPseudoRegret_of_finiteMeasureBanditRLProof.StochasticGradientBandit.twoArmStepOneStarvationEvent_charge_mul_probability_le_integralBanditRLProof.StochasticGradientBandit.twoArmFixedIIDStepOneStarvationEvent_charge_mul_probability_le_integralBanditRLProof.StochasticGradientBandit.twoArmPrefixGeneratedActionBanditRLProof.StochasticGradientBandit.twoArmPrefixOptimalPullCountBanditRLProof.StochasticGradientBandit.measurable_twoArmPrefixGeneratedActionBanditRLProof.StochasticGradientBandit.measurable_twoArmPrefixOptimalPullCountBanditRLProof.StochasticGradientBandit.twoArmPrefixOptimalPullCount_environmentPrefix_eqBanditRLProof.StochasticGradientBandit.twoArmInclusiveOptimalPullCountProcessBanditRLProof.StochasticGradientBandit.adapted_twoArmInclusiveOptimalPullCountProcessBanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullTimeBanditRLProof.StochasticGradientBandit.isStoppingTime_twoArmNthOptimalPullTimeBanditRLProof.StochasticGradientBandit.measurable_twoArmNthOptimalPullTimeBanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullTime_eq_top_iffBanditRLProof.StochasticGradientBandit.twoArmOptimalPullCount_lt_succ_of_nthOptimalPullTime_eq_topBanditRLProof.StochasticGradientBandit.twoArmOptimalPullCount_lt_of_fin_nthOptimalPullTime_eq_topBanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullTime_count_succ_eqBanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullTime_count_succ_eq_of_eqBanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullTime_action_eq_zeroBanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullTime_count_eqBanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullTime_specBanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullRewardBanditRLProof.StochasticGradientBandit.adapted_twoArmGeneratedRewardBanditRLProof.StochasticGradientBandit.measurable_twoArmNthOptimalPullRewardBanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullReward_eq_of_time_eqBanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullSuccessProbabilityBanditRLProof.StochasticGradientBandit.adapted_twoArmSuccessProbabilityBanditRLProof.StochasticGradientBandit.measurable_twoArmNthOptimalPullSuccessProbabilityBanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullSuccessProbability_eq_of_time_eqBanditRLProof.UCB.armStreamMeasure_map_fixedArmFinitePrefix_eq_piBanditRLProof.Thompson.latentArmStreamTrajectoryMeasure_map_fixedArmFinitePrefix_eq_piBanditRLProof.StochasticGradientBandit.twoArmFixedIIDLatentTrajectoryMeasureBanditRLProof.StochasticGradientBandit.twoArmTrajectoryMeasure_dirac_eq_map_trajectoryKernelBanditRLProof.StochasticGradientBandit.stationaryRewardKernelAt_twoArmFixedIIDRewardKernel_eqBanditRLProof.StochasticGradientBandit.twoArmFixedIIDLatentTrajectoryMeasure_map_optimalPrefix_eq_piBanditRLProof.StochasticGradientBandit.twoArmNthOptimalPullReward_eq_latentCoordinate_aeBanditRLProof.UCB.armStreamMeasure_map_frestrictLe_eq_piBanditRLProof.UCB.extendArmStreamFinitePrefixBanditRLProof.UCB.measurable_extendArmStreamFinitePrefixBanditRLProof.UCB.extendArmStreamFinitePrefix_apply_of_leBanditRLProof.Thompson.latentArmStreamTrajectoryKernel_map_frestrictLe_eq_of_streamPrefix_eqBanditRLProof.Thompson.latentArmStreamVisiblePrefixKernelBanditRLProof.Thompson.latentArmStreamTrajectoryKernel_map_frestrictLe_eq_prefixKernel_comapBanditRLProof.Thompson.latentArmStreamTrajectoryMeasure_map_stream_visiblePrefix_eqBanditRLProof.UCB.armStreamMeasure_map_output_coordinate_compProd_comap_without_eq_prodBanditRLProof.Thompson.latentArmStreamVisiblePrefixNextActionBanditRLProof.Thompson.measurable_latentArmStreamVisiblePrefixNextActionBanditRLProof.Thompson.latentArmStreamVisibleNextRewardBanditRLProof.Thompson.measurable_latentArmStreamVisibleNextRewardBanditRLProof.Thompson.latentArmStreamVisiblePrefixNextActionBranchKernelBanditRLProof.Thompson.latentArmStreamPrefixCountCapBanditRLProof.Thompson.measurableSet_latentArmStreamPrefixCountCapBanditRLProof.Thompson.realHistoryPullCount_extendPairHistorySuccBanditRLProof.Thompson.LatentArmStreamVisiblePrefixNextActionBranchLocalityBanditRLProof.Thompson.latentArmStreamVisiblePrefixNextAction_coordinate_branch_eq_prod_of_localityBanditRLProof.Thompson.latentArmStreamTrajectoryMeasure_map_visiblePrefix_nextAction_eq_compProdBanditRLProof.Thompson.latentArmStreamVisibleNextReward_eq_selectedCoordinate_aeBanditRLProof.Thompson.latentArmStreamTrajectoryKernel_map_prefix_next_eq_compProdBanditRLProof.Thompson.latentArmStreamFeedback_eq_of_withoutCoordinate_eq_of_selectedCoordinate_neBanditRLProof.Thompson.historyStepKernel_apply_eq_of_withoutCoordinate_eq_of_target_count_ltBanditRLProof.Thompson.latentArmStreamNextActionNeSetBanditRLProof.Thompson.latentArmStreamInitialSafeArmSetBanditRLProof.Thompson.measurableSet_latentArmStreamNextActionNeSetBanditRLProof.Thompson.historyStepKernel_apply_restrict_nextActionNe_eq_of_withoutCoordinate_eqBanditRLProof.Thompson.latentArmStreamTrajectoryKernel_map_frestrictLe_zeroBanditRLProof.Thompson.singletonPairHistory_preimage_latentArmStreamPrefixCountCap_zeroBanditRLProof.Thompson.latentArmStreamPrefixCountCapLocality_zeroBanditRLProof.Thompson.latentArmStreamPrefixCountLtBanditRLProof.Thompson.measurableSet_latentArmStreamPrefixCountLtBanditRLProof.Thompson.latentArmStreamPrefixCountEqBanditRLProof.Thompson.measurableSet_latentArmStreamPrefixCountEqBanditRLProof.Thompson.mem_latentArmStreamPrefixCountCap_extendPairHistorySucc_iffBanditRLProof.Thompson.latentArmStreamPrefixCountCap_of_extendPairHistorySucc_memBanditRLProof.Thompson.selectedCoordinate_ne_of_extendPairHistorySucc_mem_prefixCountCapBanditRLProof.Thompson.latentArmStreamSuccessorCountCap_preimageBanditRLProof.Thompson.latentArmStreamSuccessorCountCapSectionBanditRLProof.Thompson.measurableSet_latentArmStreamSuccessorCountCapSectionBanditRLProof.Thompson.historyStepKernel_apply_restrict_successorCountCap_eq_of_withoutCoordinate_eqBanditRLProof.Thompson.latentArmStreamTrajectoryKernel_map_frestrictLe_restrict_countCap_succBanditRLProof.Thompson.latentArmStreamTrajectoryKernel_map_frestrictLe_restrict_countCap_eq_of_withoutCoordinate_eqBanditRLProof.Thompson.latentArmStreamVisiblePrefixNextActionBranchLocality_of_prefixCountCapLocalityBanditRLProof.Thompson.latentArmStreamVisiblePrefixNextActionBranchLocalityBanditRLProof.Thompson.latentArmStreamVisiblePrefixNextAction_coordinate_branch_eq_prodBanditRLProof.Thompson.measurable_latentArmStreamSelectedCoordinateBanditRLProof.Thompson.latentArmStreamVisiblePrefixNextAction_selectedCoordinate_branch_eq_prodBanditRLProof.Thompson.latentArmStreamVisiblePrefixNextAction_selectedCoordinate_mixed_eq_compProdBanditRLProof.Thompson.latentArmStreamVisiblePrefixNextAction_selectedCoordinate_eq_compProdBanditRLProof.Thompson.latentArmStreamVisibleNextReward_joint_eq_compProdBanditRLProof.Thompson.latentArmStreamVisibleNextReward_condDistrib_ae_eq_nuBanditRLProof.Thompson.latentArmStreamVisibleTrajectoryMeasure_nextReward_joint_eq_compProdBanditRLProof.Thompson.latentArmStreamVisibleTrajectoryMeasure_nextReward_condDistrib_ae_eq_nuBanditRLProof.Measure.compProd_restrict_eq_of_base_restrict_eq_of_fiber_restrict_eqBanditRLProof.Measure.map_compProd_restrict_eq_of_base_restrict_eq_of_fiber_restrict_eq`	A bridge from the compiled terminal-count-below event to a fixed-cutoff starvation trigger/event; the exact probability split and missing-pull-to-terminal-count inclusion do not supply occurrence-conditioned IID. The stopped-prefix future-cylinder law needed to prove conditional no-return probability at least one half; one-step fixed-history action kernels do not supply that law. The Rademacher/binomial anti-concentration and ballot-prefix phase producer, followed by the finite-to-asymptotic polynomial-regret assembly. The frozen terminal twoArmRademacherDirac_theoremTwo_polynomialRegret; Corollary 1 and the compiled nth-pull, latent product/readout, finite-prefix factorization, branch-locality, one-step freshness, full native-law, masked selected-block, exact phase-event, phase dichotomy, missing-pull-to-terminal-count, and deterministic starvation layers are not terminal evidence.
Balanced target-drift controlled evaluation	Planned	No local declaration yet	Freeze the provider, operator-attested immutable model version, exact Codex CLI provider-client bytes/version, auth-only runtime boundary, reasoning effort, service tier, sampling semantics, dated cache-read/cache-write/input/output token prices, replicate semantics, and token/tool/build/time/cost budgets; hash-seal the implemented missing-run policy and completion-ledger builder, keep the adapter to one CLI invocation, and explicitly freeze or disclose the provider-client-internal retry boundary. Publish and freeze the final production checker image from the reviewed ephemeral candidate, freeze the provider image and commands, and reseal all seven bound checker probes under that final published image; the result-free candidate run passed the same seven probes but is not the final production seal. Extend the result-free-only root PID-1/control/credential boundary candidate with a separately reviewed real-execution action, freeze its auth/visibility/network/tool/active-budget boundaries, publish and re-pull the final digest, and rerun all bound probes; only then run the implemented, hash-bound real-provider/real-sandbox one-case-by-three-condition smoke lane, whose operator-only plan and checker state permanently force result_eligible=false and exclude it from the 450, blind grading, and inferential 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 the resulting internal-pack and grader-only-export digests. Complete the separately pinned and still-unrun LeanFlow external-system calibration: first freeze its adapter, schedule, fairness boundary, graders, and analysis, then pass its result-ineligible smoke, and only then execute the planned 30-run descriptive comparison without pooling it into the 450-run primary estimand. Execute and neutrally check all 450 matched runs, complete independent grading, and analyze the frozen target-level endpoints.

Open boundaries

The conservative generated KL-UCB finite-time route has named compiled declarations. The source-frozen delayed-bandit audit now compiles accounting, causal-view, new-arrival processing, probability allocation, the deterministic optimal-arm-survival core, and a causal one-round action measure. EAP/BSC state preservation, a measurable recursive trajectory, and stochastic/adversarial regret endpoints remain blocked. The source-frozen succinct-lower-bound audit compiles 54 declarations covering Definitions 3.1–3.3 and Lemmas 3.1–3.4, including the finite-Bessel strict-support route, plus an explicit global-R boundedness diagnostic; the global Lemmas 3.5–3.6 and Theorem 3.8 remain open. The stochastic-gradient-bandit audit retains the exact counted 361 = 223 + 23 + 25 + 26 + 7 + 8 + 13 + 28 + 8 audit-slice inventory through deterministic-time selected-reward freshness, terminal-count events, nth-pull-to-count bridges, and a generic low-count regret consumer. A separate ten-declaration module proves equality of the complete visible/native trajectory measures. The selected-block module now contains eight declarations for missing-pull-aware block transport, fourteen for the exact finite Appendix-C `S0/S1` event, ten for the exact disjoint all-present/missing-pull probability split, and four for missing-pull inclusion, visible-marginal probability transport, and the finite-horizon expected-regret charge. None is a selected-IID theorem or a positive-probability producer. Corollary 1 remains a direct Theorem-1 consumer, not Theorem-2 evidence. The frozen K = 2 Theorem-2 terminal remains blocked: the generated all-present phase still needs a fixed-chronological-cutoff trigger, the stopped-prefix future-cylinder law must yield conditional no-return probability at least one half, and the Rademacher/ballot probability plus asymptotic assembly remain uncompiled. The frozen terminal twoArmRademacherDirac_theoremTwo_polynomialRegret is not claimed. The Theorem-4 terminal also remains blocked because the general-K generated process, uniform buffer/survival producer, stopped-process argument, and regret assembly are absent. Full BwK/primal-dual regret, dueling, robust, federated, and neural-bandit routes remain planned or partial.
Direct LeanMachineLearning declaration identity remains blocked on a deliberate cross-toolchain migration and real upstream-symbol import; local theorem-card-shaped ETC/UCB proofs do not satisfy that gate.
The harness records completion gates but does not replace Lean elaboration or mathematical review.

All Lean modules in this chapter

Open the complete module list (41 modules)

Module	Declarations	Project imports	Status
`BanditRLProof.Algorithms.StochasticGradientBanditAudit`	26	0	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditConditionalExponentialAudit`	4	2	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditCorollaryOne`	23	1	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditExponentialAudit`	14	1	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTheoremFourContractAudit`	8	1	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTheoremTwoLatentReward`	7	3	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTheoremTwoNativePrefix`	9	1	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTheoremTwoNativeTrajectory`	55	5	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTheoremTwoNthPull`	26	2	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTheoremTwoSelectedIID`	43	1	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTheoremTwoStarvation`	26	4	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTrajectoryAudit`	18	2	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTwoArmFixedIID`	9	3	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTwoArmInitialRecurrence`	3	1	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTwoArmMeasurableRecurrence`	25	1	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTwoArmPathIntegrability`	19	2	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTwoArmRate`	18	1	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTwoArmRecurrence`	10	1	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTwoArmTheoremOne`	32	2	Compiled
`BanditRLProof.Algorithms.StochasticGradientBanditTwoArmUnconditionalRecurrence`	37	1	Compiled
`BanditRLProof.Automation`	9	1	Compiled
`BanditRLProof.BudgetStoppingTime`	3	0	Compiled
`BanditRLProof.DelayedFeedback.Accounting`	17	0	Compiled
`BanditRLProof.DelayedFeedback.ActionLaw`	10	2	Compiled
`BanditRLProof.DelayedFeedback.ActiveAllocation`	8	1	Compiled
`BanditRLProof.DelayedFeedback.CausalView`	11	1	Compiled
`BanditRLProof.DelayedFeedback.EliminatedArmInitialization`	31	1	Compiled
`BanditRLProof.DelayedFeedback.Elimination`	9	1	Compiled
`BanditRLProof.DelayedFeedback.MultiRegimeContract`	5	0	Compiled
`BanditRLProof.DelayedFeedback.OrderedNoSwitchTrace`	12	1	Compiled
`BanditRLProof.DelayedFeedback.OrderedProcessingTransition`	15	2	Compiled
`BanditRLProof.DelayedFeedback.ProcessedPrefixCounts`	16	1	Compiled
`BanditRLProof.DelayedFeedback.Processing`	9	1	Compiled
`BanditRLProof.DelayedFeedback.RecursiveProcessedState`	9	1	Compiled
`BanditRLProof.DelayedFeedback.StochasticGapHalfSet`	6	0	Compiled
`BanditRLProof.DelayedFeedback.StochasticGapOrderingAudit`	19	1	Compiled
`BanditRLProof.DelayedFeedback.StochasticGoodEvent`	11	2	Compiled
`BanditRLProof.DelayedFeedback.StochasticGoodEventAssembly`	14	2	Compiled
`BanditRLProof.Literature`	3	3	Compiled
`BanditRLProof.LowerBounds.SuccinctGeometryAudit`	54	0	Compiled
`BanditRLProof.OpenProblems`	3	1	Compiled