Theorem 10, first claim — no spin-block algorithm is competitive within a factor less than
ProvedNonuniformCompetitive.SpinBlock.no_better_ratioLet be the context-switch cost of the spin-block problem. If a randomized on-line algorithm (a probability distribution over deterministic on-line algorithms, each choosing the blocking time for the next lock wait from the release times of the previous ones) is -competitive against an oblivious adversary, that is, for some constant and every finite sequence of lock waits
then
This is the lower-bound half of Theorem 10: no algorithm, deterministic or randomized, beats the factor against an oblivious adversary, while deterministic algorithms cannot beat .
Formalization Note The statement quantifies over every randomized algorithm and every factor ; deterministic algorithms are the point masses. The additive constant is part of competitiveness, so the bound concerns long sequences of lock waits, not a single wait. On-line algorithms may use the release times of earlier waits, which only strengthens the lower bound. The hypothesis is the paper's "some large cost ".
import Mathlib import Definitions.Def_NonuniformCompetitive_SpinBlock_Randomized
namespace NonuniformCompetitive.SpinBlock
/-- Theorem 10, first claim (p. 559): no algorithm for the spin-block problem is competitive
against an oblivious adversary within a factor less than `e/(e − 1)`. -/
theorem no_better_ratio (C : ℝ) (hC : 0 < C) (A : RandomizedAlg C) (c : ℝ)
(hA : A.IsCompetitive c) :
Real.exp 1 / (Real.exp 1 - 1) ≤ c := by sorry
end NonuniformCompetitive.SpinBlock
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.