Part IV — Lower Bounds for Bandits with Finitely Many Arms

Chapter 13: Lower Bounds: Basic Ideas

Theorem 13.1 compiles through Chapter 15 with c=1/54. Chapter 13 also compiles fixed-class minimax-optimality, the canonical iid Gaussian empirical-mean law, midpoint error events, the Chernoff companion, and both exact Mills-ratio bounds of Eq. (13.4) rescaled to the printed Eq. (13.1). The broader 1-subgaussian class with gaps in [0,1] now has a compiled fixed-horizon MOSS upper bound and constant-factor near-minimax theorem. The frozen main-text contract is complete: PR #105, authoritative-main checks, Pages deployment and live desktop/mobile acceptance pass for b38630c. Notes and Exercises remain optional and unformalized.

Compiled theorem routeCompiled

Whole main-text contractCompiled

Printed pp. 155–159PDF pp. 189–194

Source map

Bandit Algorithms, Tor Lattimore and Csaba Szepesvári, Cambridge University Press (2020), DOI 10.1017/9781108571401.

§13.1 Main Ideas Underlying Minimax Lower Bounds (CUP starts p. 155 / author-online pp. 181–182 / PDF pp. 190–191)
§13.2 Notes (CUP p. 158 / author-online p. 183 / PDF p. 192)
§13.3 Bibliographic Remarks (CUP p. 158 / author-online p. 184 / PDF p. 193)
§13.4 Exercises (CUP p. 159 / author-online pp. 184–185 / PDF pp. 193–194)

Section coverage

Section	Status	Formalization boundary
Chapter opening and Theorem 13.1	Compiled	Worst-case/minimax semantics, fixed-class minimax-optimality, and the unit-Gaussian c=1/54 theorem endpoint compile.
§13.1 Main Ideas Underlying Minimax Lower Bounds	Compiled	The canonical iid Gaussian empirical-mean law, midpoint error events, exact two-sided Eq. (13.1), least-explored-arm selection, one-coordinate construction, regret identities, history transport, tuning, and the final lower terminal compile. The Chernoff maximum-risk companion remains separately labeled.
§13.2 Notes	Source indexed	Game interpretation, flat-risk discussion, Pareto optimality, and rate terminology are indexed as optional enrichment and are not formalized.
§13.3 Bibliographic Remarks	Source indexed	The Abramowitz–Stegun source is mapped; both exact integral bounds of Eq. (13.4) compile in GaussianMillsRatio.lean.
§13.4 Exercises	Source indexed	Exercises 13.1 and 13.2 are indexed as explicitly optional and unformalized.

Open Chapter 13 at PDF p. 189

Learning goals

Read worst-case and minimax expected regret as explicit supremum and infimum operations.
Read minimax optimality as attainment relative to a policy class, environment class, and horizon-indexed regret functional.
Trace the canonical finite iid Gaussian product through summation and scaling to the exact N(mu,1/n) empirical-mean law.
Trace both compiled Mills-ratio integral bounds through Gaussian density standardization to the exact two-sided Eq. (13.1); distinguish the weaker Chernoff companion.
Derive a least-explored alternative arm from the exact expected pull-count budget.
Separate the deterministic two-environment regret algebra from the statistical change-of-measure bridge supplied in Chapters 14–15.
Trace how the exact Chapter 15 factor 1/27 yields Theorem 13.1 with the explicit universal constant 1/54.

Necessary definitions and statements

Worst-case and minimax expected regret

Compiled

Worst-case and minimax expected regret. Formula renderer unavailable; readable fallback: The minimax value is the infimum over policies of their worst expected regret over the environment class.\[R_n^*(\mathcal E)=\inf_{\pi}\sup_{\nu\in\mathcal E}R_n(\pi,\nu).\]

Minimax-optimal policy

Compiled

Minimax-optimal policy. Formula renderer unavailable; readable fallback: A policy is minimax optimal only for fixed admissible classes and a fixed-horizon regret functional, and only if it attains the infimum.\[\pi\in\mathcal P,\qquad R_n(\pi,\mathcal E)=R_n^*(\mathcal P,\mathcal E).\]

Gaussian iid mean and midpoint test companion

Compiled

Gaussian iid mean and midpoint test companion. Formula renderer unavailable; readable fallback: The arithmetic mean under the canonical product of n independent unit-variance Gaussians has variance one over n, and the midpoint rule has the standard Chernoff maximum-error upper bound. The latter remains weaker than Eq. (13.1).\[\overline X_n\sim\mathcal N(\mu,1/n),\qquad \max_{\mu\in\{0,\Delta\}}\mathbb P_{\mathcal N(\mu,1/n)}(\hat\mu\neq\mu)\le\exp(-n\Delta^2/8).\]

Least-explored alternative

Compiled

Least-explored alternative. Formula renderer unavailable; readable fallback: Among the m alternatives, at least one is pulled no more than the average n divided by m.\[\sum_{a=0}^{m}\mathbb E[T_a(n)]=n\Longrightarrow\exists i\in\{1,\ldots,m\}:\mathbb E[T_i(n)]\le n/m.\]

Two-environment algebra

Compiled

Two-environment algebra. Formula renderer unavailable; readable fallback: A quantitative upper bound on the pull-count discrepancy leaves a matching error term in the two-environment regret lower bound.\[x-y\le\varepsilon\Longrightarrow\max\{\Delta(n-x),\Delta y\}\ge\tfrac{\Delta(n-\varepsilon)}{2}.\]

proof pseudocode

Minimal source-change proof flow

Choose the base instance
Give arm zero mean Delta and every alternative mean zero.
Find a lightly sampled alternative
Use the expected pull budget to choose i.succ with expected count at most n/m.
Change one source
Raise only that alternative mean to 2 Delta; keep the policy fixed.
Write both regret expressions
Expose the base identity and changed-environment lower expression without identifying their expectations.
Apply indistinguishability
The compiled Chapter 15 history KL and Chapter 14 Bretagnolle–Huber theorem turn the lightly sampled alternative into a quantitative minimax conclusion.

Key source theorem and boundary

Source theorem · faithful restatement

Theorem 13.1 (source statement; proof deferred to Chapter 15)

Original chapter ↗Compiled

The source states the finite-arm Gaussian minimax order here and explicitly postpones its proof to Chapter 15.

Theorem 13.1 (source statement; proof deferred to Chapter 15). Formula renderer unavailable; readable fallback: For unit-variance k-armed Gaussian bandits with means in the unit cube, minimax regret is at least a universal constant times the square root of k times n.\[\exists c>0\;\forall k>1\;\forall n\ge k:\quad R_n^*(\mathcal E^k)\ge c\sqrt{kn},\]

Lean boundary. BanditRLProof.LowerBounds.unitGaussianMinimaxExpectedPseudoRegret_ge_one_div_fiftyFour_sqrt compiles the source order statement for the same unit-cube, unit-variance Gaussian environment class with the explicit positive constant c=1/54. The local expected regret is an ENNReal lower integral on the canonical n-observation history law.

Lean correspondence

Only declarations that exist in the current index and pass the verified build may render as compiled.

Lean declaration	Status	Role and exact type
`BanditRLProof.MOSS.canonicalGapExpectedRegret_le`	Compiled	Fixed-horizon Algorithm 7 bound 39 sqrt(nk) plus the gap sum on the actual canonical history law. Exact compact Lean statement theorem canonicalGapExpectedRegret_le {k : ℕ} [NeZero k] (hk : 0 < k) (ν : Kernel (Fin k) ℝ) [IsMarkovKernel ν] (t : ℕ) (hkt : k ≤ t+1) (mean : Fin k → ℝ) (best : Fin k) (hbest : ∀ a, mean a ≤ mean best) (hmean : ∀ a, ∫ r, r ∂ν a = mean a) (hsubG : ∀ a, HasSubgaussianMGF (fun r => r-mean a) 1 (ν a)) : LowerBounds.canonicalGapExpectedPseudoRegretReal (historyAlgorithm hk (t+1)) ν (fun a => mean best-mean a) t ≤ 39Real.sqrt (((t+1 : ℕ) : ℝ)k) + ∑ a, (mean best-mean a)
`BanditRLProof.LowerBounds.subgaussianMinimax_sandwich`	Compiled	For unit-subgaussian arms with gaps in [0,1], lower constant 1/54 and MOSS upper constant 40, using identical policy and regret semantics. Exact compact Lean statement `theorem subgaussianMinimax_sandwich {k : ℕ} [NeZero k] (hk : 1 < k) (t : ℕ) (hkt : k ≤ t+1) : ENNReal.ofReal ((1/54 : ℝ)Real.sqrt ((k : ℝ)(t+1))) ≤ subgaussianMinimaxExpectedPseudoRegret k t ∧ subgaussianMinimaxExpectedPseudoRegret k t ≤ subgaussianWorstCaseExpectedPseudoRegret k (MOSS.historyAlgorithm (by omega) (t+1)) t ∧ subgaussianWorstCaseExpectedPseudoRegret k (MOSS.historyAlgorithm (by omega) (t+1)) t ≤ ENNReal.ofReal (40Real.sqrt ((k : ℝ)(t+1)))`
`BanditRLProof.LowerBounds.moss_nearMinimax`	Compiled	Main-prose constant-factor near-minimax consequence: MOSS worst-case regret is at most 2160 times minimax regret; k>1 and n>=k. Exact compact Lean statement `theorem moss_nearMinimax {k : ℕ} [NeZero k] (hk : 1 < k) (t : ℕ) (hkt : k ≤ t+1) : subgaussianWorstCaseExpectedPseudoRegret k (MOSS.historyAlgorithm (by omega) (t+1)) t ≤ 2160 * subgaussianMinimaxExpectedPseudoRegret k t`
`BanditRLProof.Concentration.measure_exists_le_independent_partialSum_ge_le_subgaussian`	Compiled	Finite maximal independent centered subgaussian bound with no cardinality loss, consumed by compiled MOSS peeling and regret integration. Exact compact Lean statement `theorem measure_exists_le_independent_partialSum_ge_le_subgaussian (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (hind : iIndepFun X μ) (hmean : ∀ i, ∫ ω, X i ω ∂μ = 0) (c : ℝ≥0) (hc : 0 < (c : ℝ)) (hsubG : ∀ i, HasSubgaussianMGF (X i) c μ) (n : ℕ) (hn : 0 < n) (ε : ℝ) (hε : 0 < ε) : μ {ω \| ∃ i, i ≤ n ∧ ε ≤ ∑ j ∈ range i, X (j + 1) ω} ≤ ENNReal.ofReal (exp (-(ε ^ 2) / (2 * (n : ℝ) * (c : ℝ))))`
`BanditRLProof.MOSS.historyAlgorithm`	Compiled	Concrete measurable fixed-horizon Algorithm 7 history policy, used by the compiled common-history expected-regret theorem. Exact compact Lean statement `noncomputable def historyAlgorithm {k : ℕ} (hk : 0 < k) (n : ℕ) : Thompson.HistoryAlgorithm (Fin k) ℝ where`
`BanditRLProof.MOSS.selected_index_gt_mean_add_half_gap`	Compiled	Deterministic large-gap selection step under an explicit optimism-deficit premise, not a concentration bound. Exact compact Lean statement `theorem selected_index_gt_mean_add_half_gap {k : ℕ} (hk : 0 < k) (n t : ℕ) (mean empiricalMean : Fin k → ℝ) (pulls : Fin k → ℕ) (best chosen : Fin k) (deficit : ℝ) (ht : k ≤ t) (hselected : action hk n t empiricalMean pulls = chosen) (hoptimism : mean best - deficit ≤ index n empiricalMean pulls best) (hgap : 2 * deficit < mean best - mean chosen) : mean chosen + (mean best - mean chosen) / 2 < index n empiricalMean pulls chosen`
`BanditRLProof.LowerBounds.gaussianMills_lower_integral`	Compiled	Exact lower integral bound of Eq. (13.4). Exact compact Lean statement `theorem gaussianMills_lower_integral {x : ℝ} (hx : 0 ≤ x) : Real.exp (-x ^ 2) / (x + Real.sqrt (x ^ 2 + 2)) ≤ ∫ t in Ioi x, Real.exp (-t ^ 2)`
`BanditRLProof.LowerBounds.gaussianMills_upper_integral`	Compiled	Exact upper integral bound of Eq. (13.4), with denominator constant 4/pi. Exact compact Lean statement `theorem gaussianMills_upper_integral {x : ℝ} (hx : 0 ≤ x) : (∫ t in Ioi x, Real.exp (-t ^ 2)) ≤ Real.exp (-x ^ 2) / (x + Real.sqrt (x ^ 2 + 4 / Real.pi))`
`BanditRLProof.LowerBounds.gaussianSampleMeanZeroErrorProbability_source_bounds`	Compiled	Exact printed Eq. (13.1) for n>0 and Delta>0, with denominator constants 16 and 32/pi. Exact compact Lean statement `theorem gaussianSampleMeanZeroErrorProbability_source_bounds (sampleSize : Nat) (hsampleSize : 0 < sampleSize) (gap : Real) (hgap : 0 < gap) : let q := (sampleSize : Real) * gap ^ 2 Real.sqrt (8 / Real.pi) * Real.exp (-q / 8) / (Real.sqrt q + Real.sqrt (q + 16)) ≤ gaussianSampleMeanZeroErrorProbability sampleSize gap ∧ gaussianSampleMeanZeroErrorProbability sampleSize gap ≤ Real.sqrt (8 / Real.pi) * Real.exp (-q / 8) / (Real.sqrt q + Real.sqrt (q + 32 / Real.pi))`
`BanditRLProof.LowerBounds.worstCaseExpectedRegret`	Compiled	Worst-case ENNReal supremum over an explicit environment class. Exact compact Lean statement `noncomputable def worstCaseExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (environmentClass : Set Environment) (policy : Policy) : ENNReal`
`BanditRLProof.LowerBounds.minimaxExpectedRegret`	Compiled	Minimax ENNReal infimum over an explicit policy class. Exact compact Lean statement `noncomputable def minimaxExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (policyClass : Set Policy) (environmentClass : Set Environment) : ENNReal`
`BanditRLProof.LowerBounds.IsMinimaxOptimal`	Compiled	Admissibility plus attainment for fixed policy/environment classes and a horizon-indexed regret functional. Exact compact Lean statement `def IsMinimaxOptimal {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (policyClass : Set Policy) (environmentClass : Set Environment) (policy : Policy) : Prop`
`BanditRLProof.LowerBounds.gaussianSampleMeanVariance_pos`	Compiled	Nondegenerate variance 1/n for a positive sample size. Exact compact Lean statement `theorem gaussianSampleMeanVariance_pos (sampleSize : Nat) (hsampleSize : 0 < sampleSize) : 0 < gaussianSampleMeanVariance sampleSize`
`BanditRLProof.LowerBounds.gaussianIIDObservationLaw`	Compiled	Canonical finite product law of independent N(mu,1) coordinates. Exact compact Lean statement `noncomputable def gaussianIIDObservationLaw (sampleSize : Nat) (mean : Real) : Measure (Fin sampleSize → Real)`
`BanditRLProof.LowerBounds.gaussianIIDSumLaw`	Compiled	Exact N(n mu,n) law of the coordinate sum by characteristic-function factorization. Exact compact Lean statement `theorem gaussianIIDSumLaw (sampleSize : Nat) (mean : Real) : (gaussianIIDObservationLaw sampleSize mean).map (fun observations => ∑ i, observations i) = gaussianReal ((sampleSize : Real) * mean) (sampleSize : NNReal)`
`BanditRLProof.LowerBounds.gaussianIIDSampleMeanLaw`	Compiled	Exact N(mu,1/n) pushforward law of the arithmetic mean for n>0. Exact compact Lean statement `theorem gaussianIIDSampleMeanLaw (sampleSize : Nat) (mean : Real) (hsampleSize : 0 < sampleSize) : (gaussianIIDObservationLaw sampleSize mean).map (gaussianCoordinateAverage sampleSize) = gaussianSampleMeanLaw sampleSize mean`
`BanditRLProof.LowerBounds.twoPointGaussianThresholdDecision_zero_error_event`	Compiled	The zero-mean midpoint decision error is exactly the source event [Delta/2,infinity). Exact compact Lean statement `theorem twoPointGaussianThresholdDecision_zero_error_event {gap : Real} (hgap : 0 < gap) : {observation \| twoPointGaussianThresholdDecision gap observation ≠ 0} = Set.Ici (gap / 2)`
`BanditRLProof.LowerBounds.twoPointGaussianThresholdDecision_gap_error_event`	Compiled	The positive-mean midpoint decision error is exactly the symmetric lower-half event. Exact compact Lean statement `theorem twoPointGaussianThresholdDecision_gap_error_event {gap : Real} (hgap : 0 < gap) : {observation \| twoPointGaussianThresholdDecision gap observation ≠ gap} = Set.Iio (gap / 2)`
`BanditRLProof.LowerBounds.hasSubgaussianMGF_id_gaussianReal_zero`	Compiled	Exact Gaussian MGF supplies the centered sub-Gaussian proxy. Exact compact Lean statement `theorem hasSubgaussianMGF_id_gaussianReal_zero (variance : NNReal) : HasSubgaussianMGF id variance (gaussianReal 0 variance)`
`BanditRLProof.LowerBounds.gaussianSampleMeanThresholdRisk_le_exp`	Compiled	Source-shaped two-hypothesis maximum-risk Chernoff companion exp(-n Delta^2/8), explicitly not Eq. (13.1). Exact compact Lean statement `theorem gaussianSampleMeanThresholdRisk_le_exp (sampleSize : Nat) (gap : Real) (hgap : 0 < gap) : gaussianSampleMeanThresholdRisk sampleSize gap ≤ Real.exp (-(sampleSize : Real) * gap ^ 2 / 8)`
`BanditRLProof.LowerBounds.expectedRegret_le_worstCaseExpectedRegret`	Compiled	One member is below the class supremum. Exact compact Lean statement `theorem expectedRegret_le_worstCaseExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (environmentClass : Set Environment) (policy : Policy) (environment : Environment) (henvironment : environment ∈ environmentClass) : regret policy environment ≤ worstCaseExpectedRegret regret environmentClass policy`
`BanditRLProof.LowerBounds.minimaxExpectedRegret_le_worstCaseExpectedRegret`	Compiled	The infimum is below every admissible policy value. Exact compact Lean statement `theorem minimaxExpectedRegret_le_worstCaseExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (policyClass : Set Policy) (environmentClass : Set Environment) (policy : Policy) (hpolicy : policy ∈ policyClass) : minimaxExpectedRegret regret policyClass environmentClass ≤ worstCaseExpectedRegret regret environmentClass policy`
`BanditRLProof.LowerBounds.le_minimaxExpectedRegret`	Compiled	A uniform policywise lower bound passes through the minimax infimum. Exact compact Lean statement `theorem le_minimaxExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (policyClass : Set Policy) (environmentClass : Set Environment) (lower : ENNReal) (hlower : ∀ policy : policyClass, lower ≤ worstCaseExpectedRegret regret environmentClass policy.1) : lower ≤ minimaxExpectedRegret regret policyClass environmentClass`
`BanditRLProof.LowerBounds.exists_alternative_le_average`	Compiled	Reusable finite averaging leaf. Exact compact Lean statement `theorem exists_alternative_le_average {m : Nat} (hm : 0 < m) (alternativeExpectedPulls : Fin m -> Real) (budget : Real) (hbudget : ∑ i : Fin m, alternativeExpectedPulls i ≤ budget) : ∃ i : Fin m, alternativeExpectedPulls i ≤ budget / (m : Real)`
`BanditRLProof.LowerBounds.alternativeExpectedPullBudget_le`	Compiled	Remove the nonnegative distinguished-arm contribution from the exact total. Exact compact Lean statement `theorem alternativeExpectedPullBudget_le {m : Nat} (expectedPulls : Fin (m + 1) -> Real) (budget : Real) (hnonneg : ∀ arm, 0 ≤ expectedPulls arm) (htotal : ∑ arm : Fin (m + 1), expectedPulls arm = budget) : (∑ i : Fin m, expectedPulls i.succ) ≤ budget`
`BanditRLProof.LowerBounds.exists_leastExploredAlternative`	Compiled	Source-shaped Fin.succ alternative-arm conclusion. Exact compact Lean statement `theorem exists_leastExploredAlternative {m : Nat} (hm : 0 < m) (expectedPulls : Fin (m + 1) -> Real) (horizon : Nat) (hnonneg : ∀ arm, 0 ≤ expectedPulls arm) (htotal : ∑ arm : Fin (m + 1), expectedPulls arm = (horizon : Real)) : ∃ i : Fin m, expectedPulls i.succ ≤ (horizon : Real) / (m : Real)`
`BanditRLProof.LowerBounds.baseEnvironmentRegret`	Compiled	Equation (13.2) deterministic expression. Exact compact Lean statement `def baseEnvironmentRegret (horizon : Nat) (gap baseFirstExpectedPulls : Real) : Real`
`BanditRLProof.LowerBounds.changedEnvironmentRegretLowerBound`	Compiled	Equation (13.3) lower expression. Exact compact Lean statement `def changedEnvironmentRegretLowerBound (gap changedFirstExpectedPulls : Real) : Real`
`BanditRLProof.LowerBounds.max_base_changed_regretLowerBound_ge_half_sub_error`	Compiled	Quantitative two-environment algebra with the cross-law pull discrepancy exposed as an error premise. Exact compact Lean statement `theorem max_base_changed_regretLowerBound_ge_half_sub_error (horizon : Nat) (gap baseFirstExpectedPulls changedFirstExpectedPulls error : Real) (hgap : 0 ≤ gap) (hpullDifference : baseFirstExpectedPulls - changedFirstExpectedPulls ≤ error) : gap * ((horizon : Real) - error) / 2 ≤ max (baseEnvironmentRegret horizon gap baseFirstExpectedPulls) (changedEnvironmentRegretLowerBound gap changedFirstExpectedPulls)`
`BanditRLProof.LowerBounds.max_base_changed_regretLowerBound_ge_half`	Compiled	Zero-error directional corollary of the quantitative algebra. Exact compact Lean statement `theorem max_base_changed_regretLowerBound_ge_half (horizon : Nat) (gap baseFirstExpectedPulls changedFirstExpectedPulls : Real) (hgap : 0 ≤ gap) (htransport : baseFirstExpectedPulls ≤ changedFirstExpectedPulls) : gap * (horizon : Real) / 2 ≤ max (baseEnvironmentRegret horizon gap baseFirstExpectedPulls) (changedEnvironmentRegretLowerBound gap changedFirstExpectedPulls)`
`BanditRLProof.LowerBounds.unitGaussianMinimaxExpectedPseudoRegret_ge_one_div_fiftyFour_sqrt`	Compiled	Chapter 13 source-order terminal, derived from the exact Chapter 15 theorem with c=1/54. Exact compact Lean statement `theorem unitGaussianMinimaxExpectedPseudoRegret_ge_one_div_fiftyFour_sqrt {k horizon : Nat} (hk : 1 < k) (hkhorizon : k ≤ horizon) : ENNReal.ofReal ((1 / 54 : Real) * Real.sqrt ((k : Real) * (horizon : Real))) ≤ unitGaussianMinimaxExpectedPseudoRegret k (horizon - 1)`

Dependency graph

minimaxminimax / worst-case semanticsCompiled

minimax-optimalfixed-class minimax optimalityCompiled

gaussian-iid-meanfinite iid Gaussian empirical-mean lawCompiled

gaussian-testmidpoint Gaussian error events and Chernoff upperCompiled

eq-13-1exact two-sided Mills-ratio Eq. (13.1)Compiled

budgetexpected pull budgetCompiled

leastleast-explored alternativeCompiled

algebratwo-environment algebraCompiled

transportsame-policy history KL transportCompiled

theorem-13-1Gaussian minimax terminalCompiled

moss-upperfixed-horizon MOSS common-history upper boundCompiled

broad-near-minimaxbroad-class near-minimax factor 2160Compiled

Reading path

Read the source statement and its explicit Chapter 15 proof deferral.
Inspect the minimax definitions and minimax-optimality predicate before the averaging lemma.
Inspect the finite iid Gaussian mean-law bridge and midpoint error events, then trace the exact Mills-ratio Eq. (13.1) and the separate maximum-risk Chernoff companion.
Check the Fin.succ indexing: source arms 2,…,k become Lean alternatives 0,…,m−1.
Read the quantitative algebra theorem and locate its visible cross-environment error premise.
Continue through the compiled Chapter 14 event-testing foundation and Chapter 15 Gaussian theorem, then inspect the c=1/54 order corollary.

Strict status and remaining gaps

The frozen main-text contract is complete, including the broader finite-arm 1-subgaussian near-minimax consequence. Integrated proof, rendered export, structured review, PR, main, Pages and live acceptance are recorded for b38630c.
Optional: Notes 13.2 and Exercises 13.1–13.2 are not formalized and do not block the chapter contract.