JAO Theorem 5: MDP minimax regret lower bound $\mathbb{E}[\Delta] \ge 0.015\sqrt{DSAT}$

⚠️ 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 any algorithm and any $S, A \ge 10$, $D \ge 20\log_A S$ and $T \ge DSA$, there is an MDP with $S$ states, $A$ actions and diameter at most $D$ on which, from every initial state, the expected regret after $T$ steps is at least $0.015\sqrt{DSAT}$.

The proof splits on the size of the diameter. When $D \ge 12$ one has $\delta = 4/D \le 1/3$ and JAO's main construction applies: a two-state gadget replicated $\lceil S/2 \rceil$ times, the copies joined by an $A'$-ary tree on the $s_\circ$-states, which is then collapsed so that the analysis reduces to a bandit problem. When $D < 12$ the assumptions force $A > 2S$ and a different construction is used (JAO, footnote 11).

This is the original statement, with the explicit constant $0.015$ and the initial state universally quantified, as opposed to the Lattimore-Szepesvari restatement (Bandit Algorithms, Theorem 38.7) which asserts the bound for $S \ge 3$, $A \ge 2$ with an unspecified universal constant. The hypothesis $S, A \ge 10$ is not cosmetic: JAO's construction uses a two-state gadget with $A' = \lceil (A-1)/2 \rceil$ actions together with $A'+1$ further actions per state to connect the copies, so at $A = 2$ the construction does not exist, and the final constant is obtained from $kA' \ge 20$.

⚠ Not provable from the source as stated — see below. The constant $0.015$ on $\sqrt{DSAT}$ does not follow from JAO Section 6. The proof ends at $0.015\sqrt{D'kA'T}$ with $D' = D/4$, $k = \lfloor S/2\rfloor$, $A' = \lfloor (A-1)/2\rfloor$; since the composite MDP must fit in $S$ states and $A$ actions, $2k \le S$ and $2A'+1 \le A$, hence $D'kA' \le DSA/16$ and the proven bound is at most $0.0039\sqrt{DSAT}$. The exact supremum over $S, A \ge 10$ is $0.015/\sqrt{22} = 0.00320$, attained at $(S,A) = (11,10)$. The rest of Section 6 is correct: its bracket at $kA' = 20$ evaluates to $0.016660 > 0.015$ as claimed. The error is a single unstated substitution $D'kA' \to DSA$ in the final line.

This node is kept only as a record of the statement as published. Work instead on BanditAlgorithm.mdp_regret_lower_bound_jao_universal_constant, which carries the same hypotheses and the same $\sqrt{DSAT}$ scaling with a universal but unspecified constant. See mission comment afe04135 for the full computation.

Why this node was retired

The posted statement is

theorem BanditAlgorithm.mdp_regret_lower_bound_jao :
    ∀ S A T : ℕ, ∀ D : ℝ, 10 ≤ S → 10 ≤ A →
      20 * (Real.log S / Real.log A) ≤ D → D * S * A ≤ (T : ℝ) →
        ∀ π : MDPPolicy S A,
          ∃ M : FiniteMDP S A,
            mdpDiameterENN M ≤ ENNReal.ofReal D ∧
            ∀ s : Fin S,
              0.015 * Real.sqrt (D * S * A * T) ≤
                ∫ h, mdpRegret M T h ∂(mdpMeasure M (mdpStateDirac s) π T) := by
  sorry

The source diameter parameter is natural/at least one, but the formal parameter is real and can be 1/2 although every MDP with two states has diameter≥1.

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

Proposed corrected statement

Require D∈ℕ with D≥1, or add the explicit hypothesis 1≤D while retaining the source size and horizon conditions.

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.