$T_i(n) \le \kappa_i$ when $2\tilde\Delta < \Delta_i$

⚠️ 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.

Under MOSS, on the event that an arm's suboptimality gap exceeds twice the optimal arm's index shortfall, the arm's pull count is dominated by its MOSS index count:

almost surely under the canonical bandit measure. Here $\tilde\Delta$ is the amount by which the optimal arm's MOSS index ever drops below its true mean, and $i^{*}$ is an optimal arm.

This is the justification given on printed p. 126 of Lattimore--Szepesvári: "for arms $i$ with $\Delta_i > 2\tilde\Delta$, the index of the optimal arm is always larger than $\mu_i + \Delta_i/2$, so $\kappa_i$ is an upper bound on $T_i(n)$." Indeed, whenever MOSS plays arm $i$ its index is maximal, hence at least the optimal arm's index, which on this event exceeds $\mu_i + \Delta_i/2$ — so that pull is counted by $\kappa_i$. The hypothesis is essential: without it the domination genuinely fails.

Why this node was retired

The posted statement is

theorem BanditAlgorithm.moss_pull_count_le_kappa_on_large_gap
    {k : ℕ} (hk : 0 < k)
    {ν : BanditAlgorithm.StochasticBandit k}
    {n : ℕ} {π : BanditAlgorithm.BanditPolicy k}
    (hπ : BanditAlgorithm.IsMOSSPolicy n π)
    (iStar : Fin k)
    (hiStar : BanditAlgorithm.banditArmMean ν iStar =
      BanditAlgorithm.banditOptimalMean ν)
    (i : Fin k) :
    ∀ᵐ h ∂(BanditAlgorithm.banditMeasure ν π n),
      2 * BanditAlgorithm.mossOptimalShortfall ν iStar h <
          BanditAlgorithm.banditGap ν i →
        (BanditAlgorithm.armPullCount i h : ℝ) ≤
          (BanditAlgorithm.mossKappa ν i h : ℝ) := by sorry

The positive-sample-size κ can be zero although initialization already pulled the arm once; the posted finite-history stream additionally distorts unavailable sample means.

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

Proposed corrected statement

Restore the full potential reward-stream definition and the source counting convention, explicitly accounting for the initialization pull (e.g. a 1+κ bound when κ counts only positive sample sizes below threshold). Retain the random large-gap event from the source and re-derive the exact comparison.

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.