MOSS large-gap arm expected pull bound

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

Fix an arm $i$ with $\Delta_i>8\sqrt{k/n}$ in a 1-subgaussian bandit and run MOSS for horizon $n\ge k>0$. Then $\Delta_i\,\mathbb E[T_i(n)]\le\Delta_i+15\sqrt{n/k}$. The source defines $\kappa_i$, proves $T_i(n)\le\kappa_i$ from the MOSS index rule, and applies Lemma 8.2 to obtain this displayed armwise bound.

Why this node was retired

The posted statement is

theorem BanditAlgorithm.moss_large_gap_arm_expected_pull_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.armPullCount i h : ℝ)) ≤
      BanditAlgorithm.banditGap ν i + 15 * Real.sqrt ((n : ℝ) / k) := by
  sorry

The source only compares pulls to κ under a random optimal-index shortfall cutoff; the target asserts an unconditional per-arm pull bound.

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

Proposed corrected statement

Retain the event Δᵢ>2Z, where Z is the optimal-arm index shortfall, in the pull-count comparison/regret decomposition; state the unconditional source estimate for ΔᵢE[κᵢ], not for ΔᵢE[Tᵢ(n)]. Use full potential streams in defining κ and Z.

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.