MOSS armwise bound $\Delta_i\mathbb E[\kappa_i] \le \Delta_i + 15\sqrt{n/k}$

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

For a $1$-subgaussian bandit with $k>0$ arms and horizon $n \ge k$ under MOSS, every arm $i$ whose suboptimality gap satisfies $\Delta_i > 8\sqrt{k/n}$ obeys the armwise estimate

where $\kappa_i$ is the MOSS index count of the arm. This is exactly the displayed chain of inequalities on printed p. 126 of Lattimore--Szepesvári: one replaces the sample size $s$ inside the logarithm by $1/\Delta_i^2$ (paying a $\Delta_i \cdot \Delta_i^{-2}$ correction for the first $\Delta_i^{-2}$ rounds where this fails), applies Lemma 8.2 together with the monotonicity of $x \mapsto x^{-1-p}\log^+(ax^2)$ for $p \in [0,1]$, and finishes with the numerical bound $1/8 + 4\log 8 + 2\sqrt{\pi \log 8} + 1 \le 15$.

Note that the statement is about the index count $\kappa_i$ and not about the pull count $T_i(n)$: the source only passes from one to the other on the event where the optimal arm's index stays high (see moss_pull_count_le_kappa_on_large_gap).

Why this node was retired

The posted statement is

theorem BanditAlgorithm.moss_large_gap_arm_expected_kappa_bound
    {k : ℕ} (hk : 0 < k)
    {ν : BanditAlgorithm.StochasticBandit k}
    (hν : BanditAlgorithm.IsSubgaussianBandit 1 ν)
    {n : ℕ} {π : BanditAlgorithm.BanditPolicy k}
    (hπ : BanditAlgorithm.IsMOSSPolicy n π) (hkn : k ≤ n)
    (i : Fin k)
    (hi : 8 * Real.sqrt ((k : ℝ) / n) < BanditAlgorithm.banditGap ν i) :
    BanditAlgorithm.banditGap ν i *
        MeasureTheory.integral
          (BanditAlgorithm.banditMeasure ν π n)
          (fun h ↦ (BanditAlgorithm.mossKappa ν i h : ℝ)) ≤
      BanditAlgorithm.banditGap ν i + 15 * Real.sqrt ((n : ℝ) / k) := by sorry

The sample-size empirical mean takes only the available finite-history rewards but divides by the requested sample size even when fewer samples exist.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Define for each arm an infinite IID potential reward stream with that arm’s law, and use the first s rewards to define μ̂ᵢ,s for every s≥1. Couple realized pulls to prefixes of these streams before applying the shortfall/κ concentration bounds.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.