PaperlayerView exact revision on arXiv

Source-linked AI summary

Gap Entropy and Almost Instance-Wise Optimal Best-Arm Identification

Jiarui Yao, Jiaxi Zhao, Xiangxin Zhou

arXiv:2609.13703v1cs.CCcs.AIcs.LG

TL;DR

Best-arm identification asks how to identify the largest-mean arm with high confidence while controlling sampling. This paper proves Chen and Li [2016]’s conjectures about the instance-wise lower bound and a single algorithm. Its lower-bound argument removes monotonicity restrictions, and its upper bound has an entropy main term without the displayed polylogarithmic factor on the two-arm term.

  • Problem

    Chen and Li [2016] conjectured that the order-oblivious instance-wise lower bound is characterized by gap-group entropy and that one algorithm attains it with only an additive two-arm term.

    Source: §1 · p. 2

  • Method

    The lower-bound proof uses a latent-variable coupling and relative entropy, while the algorithm runs successive elimination with increasing weight and sample budgets.

    Source: §1 · p. 2

  • Results

    The paper proves both conjectures, with a lower bound on the original instance without monotonicity and a uniform entropy-term upper bound without the displayed polylogarithmic factor on the two-arm term.

    Source: §2.3 · p. 5, §3 · p. 6

  • Takeaways & Limitations

    The single algorithm requires no estimates of the gaps, H, or Ent(I), and its small-active-arm penalty is charged to D rather than H.

    Source: §1 · p. 2, §2.3 · p. 5

    The upper-bound statement uses a positive truncation convention; a uniform O(D) comparison with the untruncated expression does not hold near Δ[2] = 1.

    Source: §2.3 · p. 5

Abstract

from arXiv · show

In the best-arm identification problem, we are given $n$ stochastic arms with unknown means and wish to identify the arm with the largest mean with probability at least $1-\delta$, using as few samples as possible. We consider independent Gaussian rewards with unit variance and means in $[0,1]$. Chen and Li [2016] conjectured that the instance-wise sample complexity of this problem is characterized by the gap entropy, up to an additive term arising from the two-arm problem. In this paper, we resolve their gap-entropy and almost instance-wise optimality conjectures. For an instance $I$, let $\Delta_{[i]}$ be the gap between the largest and the $i$-th largest mean, let $H(I)=\sum_{i=2}^{n}\Delta_{[i]}^{-2}$, and let Ent$(I)$ denote the entropy of the normalized complexities of its dyadic gap groups. For every $0<\delta<0.1$, we show that the order-oblivious instance-wise lower bound is $ {\Theta} (H(I)[\log(1/\delta)+Ent(I)]). $ We also give a single $\delta$-correct algorithm with expected sample complexity $ O ( H(I)[\log(1/\delta)+Ent(I)] +D\log(e+\log(e+D))),D=\Delta_{[2]}^{-2}, $ without prior knowledge of the gaps. Our lower bound removes the dyadic-gap and monotonicity restrictions of previous work, and our upper bound removes the additional polylogarithmic factor multiplying the two-arm term. Thus, a single algorithm attains the instance-wise lower bound up to an additive two-arm term. The main theorems have been formalized and proved in Lean 4.

1 Introduction

Fixed-confidence best-arm identification must find the largest-mean arm while deciding how to sample and when to stop. The paper proves both conjectures of Chen and Li [2016] about the instance-wise lower bound and a single algorithm, using lower- and upper-bound arguments that address limitations of prior work.

1 Introduction

  • The proofs address Chen et al. [2017]’s sub-instance and monotonicity restrictions, as well as a polylogarithmic factor on the two-arm term.The paper notes that transferring a sub-instance lower bound to the original instance for arbitrary algorithms requires monotonicity.Source: §1 · p. 2
  • The conjectures are proved in Chen and Li [2016]’s Gaussian model for the measurable algorithms defined in Section 2.Appendix H extends the lower-bound result to arbitrary standard Borel internal randomness and history-dependent probability kernels.Source: §1 · p. 2
  • Concurrent work by Aronow et al. [2026] also resolves both conjectures, with overlapping lower-bound arguments and different upper-bound constructions.Section 3.1 compares the results and methods.Source: §1 · p. 2
  • The lower-bound argument works on the original instance without monotonicity or bounds on sample counts on other instances.It uses symmetrization, a latent-variable coupling, and relative entropy to obtain a complexity-weighted entropy term.Source: §1 · p. 2
  • A single algorithm uses successive elimination runs and needs no gap, H, or Ent(I) estimates.Its extra summable error penalty applies only to calls with at most seven active arms, charging their sampling cost to D rather than H.Source: §1 · p. 2
  • The definitions and main theorems, including explicit constants, are formalized and verified in Lean 4 with Mathlib1.Appendix I describes the verification scope and differences between the formal proofs and the paper’s presentation.Source: §1 · p. 3

2 Problem formulation and main results

The paper specifies a Gaussian best-arm identification problem and resolves the gap-entropy and almost instance-wise optimality conjectures. Its results give an instance-wise lower bound and a single algorithm that works without gap or complexity estimates, using a positive convention for the additive two-arm term.

2.1 Observation model and statistical objective

  • An instance is a vector of arm means in [0,1] with a unique maximum; observations are independent Gaussians with unit variance.The objective is to return the best arm with probability at least 1 − δ.Source: §2.1 · p. 3

2.2 The instance-wise lower bound and the gap groups

  • The lower-bound infimum is chosen separately for each target instance, while each algorithm in it must remain correct on every admissible input.The single algorithm takes the arms and δ as inputs rather than instance-specific parameters.Source: §2.2 · p. 4, §2.3 · p. 5
  • Gap entropy weights each nonempty dyadic gap group by its share of total complexity, and is at most the logarithm of the number of nonempty groups.When K groups have equal total complexity, the example has Ent(I) = log K even though the group sizes differ.Source: §2.2 · p. 4

2.3 Main results

  • Theorem 2.1 resolves the gap-entropy conjecture for every instance in the stated model when 0 < δ < 0.1.Source: §2.3 · p. 4
  • For every 0 < δ < 0.1, one δ-correct algorithm has finite expected stopping time on every admissible instance, without receiving estimates of any gap, H, or Ent(I).Source: §2.3 · p. 5
  • The two-arm term uses a positive truncation because the untruncated expression is negative for Δ[2] in (e^-1, 1) and undefined at Δ[2] = 1.The two positive conventions are equivalent up to constants; as Δ[2] tends to zero, the term has log log(1/Δ[2]) order.Source: §2.3 · p. 5
  • The universal constants in the upper bounds are large and are not optimized.The results are stated under the positive convention for the additive two-arm term.Source: §2.3 · p. 5

3 Related work

Prior work established the confidence-dependent gap-complexity scale and studied adaptation to unknown gaps, but the gap-entropy conjectures required stronger instance-wise bounds and a single algorithm. This paper resolves both conjectures and contrasts its proofs and algorithm with a concurrent resolution.

3 Related work

  • The classical H(I) log(1/δ) lower-bound scale and the two-arm iterated-logarithmic obstruction motivate separating confidence cost from adaptation to unknown gaps.The iterated-logarithmic obstruction is asymptotic across gap values, not an additional lower bound required at every fixed instance.Source: §3 · p. 5
  • Chen et al. [2017] obtained an entropy upper bound with an extra polylogarithmic two-arm factor and a lower bound restricted to dyadic gaps or monotone algorithms; this paper removes those restrictions.The present lower bound applies to the original instance under permutation averaging, with arbitrary positive gaps and no monotonicity assumption.Source: §3 · p. 6
  • Information-allocation results characterize leading confidence costs but do not by themselves control uniform dependence on unknown gaps; this paper addresses that adaptation cost using original-instance counts and a common comparison distribution.Related approaches study adaptive sampling lower bounds, while fixed-budget guarantees and structured identification problems use different criteria or settings.Source: §3 · pp. 6–7

3.1 Concurrent resolution of the two conjectures

  • A concurrent resolution obtains the same Gaussian-instance orders and also covers independent 1-sub-Gaussian rewards, whereas this paper states its theorems for Gaussian rewards.The papers use closely related lower-bound mechanisms but different exact-gap versus dyadic-group proof choices and different upper-bound constructions.Source: §3.1 · pp. 7–8

A single algorithm.

  • The single algorithm reuses one reference estimate per scale, retains at least the empirical upper half, and penalizes calls with at most seven arms to obtain the additive two-arm cost.Its correctness analysis groups outputs by fixed nested sets of near-optimal arms and combines stochastic domination with an empirical-ordering bound.Source: A single algorithm · p. 8
  • The contribution also includes Lean 4 verification of the main statements and policy-model extensions, with the verification scope and formal-witness differences specified.The formalization covers an explicit measurable-policy treatment.Source: A single algorithm · p. 8

4 Characterizing the order-oblivious instance-wise lower bound

The lower-bound proof compares labelings of the original instance with a common two-best-arm reference experiment. Disjoint stopping events then yield the entropy contribution alongside the confidence-dependent complexity term.

Common comparison distribution

  • The comparison charges sample counts on the original instance: changing one arm to the best mean and changing another arm creates a common reference law with two best arms.Uniform labeling makes that reference law independent of the designated source gap, including when gaps have multiplicities.Source: §4 · p. 9
  • When the source and reference gaps coincide, the change-of-measure bound gives α_d ≥ 2 kl(1 − δ, δ) ≥ L, without monotonicity or transferring sample complexity across instances.All compared sample counts belong to labelings of the target instance.Source: §4 · p. 9

Disjoint stopping events

  • Disjoint stopping events under the common reference distribution bound the number of low-cost gap-group representatives, yielding the entropy lower-bound contribution.The argument selects one minimum-cost gap per nonempty group and integrates a bound on their number.Source: §4 · p. 9

Lower-bound conclusion

  • Groupwise minimization and the confidence bound combine to give a lower bound involving H and the confidence requirement.The displayed quantitative expression is incomplete in the supplied passage.Source: §4 · p. 9

L + Ent(I)

For the pointwise instance-wise upper bound, the construction may use the target’s gap-group sizes while remaining correct on every input. Its finite elimination schedule has controlled total weight and succeeds uniformly over target labelings.

Target-specific construction

  • The pointwise construction fixes the target’s group sizes as algorithmic constants, although correctness is still required on every input.This is permitted for the pointwise infimum; the later single algorithm does not know the instance’s gaps.Source: L + Ent(I) · p. 9

Weight choice

  • Weights defined from the target group sizes have total weight O(H) and normalized entropy O(…).The supplied result passage truncates the entropy bound.Source: L + Ent(I) · p. 9

Elimination calls

  • At each tolerance, a call selects a reference arm, estimates its mean, and retains arms whose fresh empirical means clear the reference estimate by d/2.A finite run aborts when a required halving fails and returns only when the retained set at the finest target scale is a singleton.Source: L + Ent(I) · p. 9

Correctness and expected cost

  • Each finite run has incorrect-return probability at most ε on every input and succeeds with probability at least 1 − ε on every labeling of the target.Fresh runs are repeated and interleaved with a globally correct fallback to ensure termination away from the target.Source: L + Ent(I) · p. 10
  • The construction’s repeated-run analysis gives an expected-sample bound uniformly over target labelings.The numerical expression is truncated in the supplied passage.Source: L + Ent(I) · p. 10

5 A single algorithm

The paper constructs one δ-correct algorithm without gap information by running budgeted elimination schedules with carefully allocated confidence. Its correctness analysis controls premature elimination, and its expected-cost analysis establishes finite stopping and the Theorem 2.2 bound.

5 A single algorithm

  • The algorithm works without the instance’s gaps, complexity, or entropy, under independent unit-variance Gaussian observations, means in [0, 1], a unique best arm, and 0 < δ < 0.1.The complete procedure and its proofs are in Appendices D–F.Source: §5 · p. 10

5.1 Sample budgets and confidence allocation

  • Runs start with all arms active and fresh observations; within a run, tolerances decrease geometrically, while deterministic budgets bound total call weight and samples.Confidence allowances across calls sum to at most γ.Source: §5.1 · pp. 10–11
  • Only calls with at most seven active arms incur the additional confidence-allocation sample penalty, directing that cost to the two-arm term rather than H.The active-set size is checked at every call, including after a stall.Source: §5.1 · p. 10
  • Each call uses a median-elimination reference estimate and fresh arm estimates, retaining a threshold set enlarged to include the empirical upper half.The numerical reference estimate is reused throughout a scale, even if its arm is removed.Source: §5.1 · pp. 10–11

5.2 Correctness via sets of near-optimal arms

  • Correctness separates reference-estimation failures and small-call errors from large-call elimination of near-optimal arms, which is bounded jointly using an empirical-ordering argument.The near-optimal sets form a fixed nested family; the resulting error charges sum to below δ.Source: §5.2 · pp. 11–12

5.3 An unconditional expected sample complexity bound

  • On a good run, scales stall only when the active-arm count is within a constant factor of the number of arms closer than the current tolerance.Repeated halvings bound call weights; deterministic budgets control trajectories outside the good event.Source: §5.3 · p. 12
  • The expected-sample analysis applies logarithmic confidence costs to the call weights and separately accounts for small-call penalties and one reference estimate per scale.The supplied passages truncate the corresponding cost expressions.Source: §5.3 · p. 12
  • The run-index series converges, proving finite expected stopping time and almost-sure termination, with the bound in Theorem 2.2 and no instance parameters supplied to the algorithm.Runs outside the good-event analysis are controlled by deterministic budgets.Source: §5.3 · p. 12

6 Conclusion

The conclusion states an order lower bound and a single algorithm that matches it up to an additive term, with proofs covering arbitrary finite instances. It also discloses the role of generative AI in the mathematical and verification work.

6 Conclusion

  • The proofs cover arbitrary finite instances without monotonicity, requiring termination at two-best-arm instances, or prior gap, complexity, or entropy estimates.Source: §6 · p. 13
  • The single algorithm matches the instance-wise lower bound up to an additive term, and the conclusion states that the lower bound is of Θ order.Source: §6 · p. 13

AI use statement

  • The main derivations and Lean 4 formalization were primarily done by gpt-6-astra, then checked by claude-fable-5.1; model-based checks are distinct from kernel checks.Source: AI use statement · p. 13

A Probabilistic and elimination preliminaries

The preliminaries establish tools that remain valid under adaptive sampling and active-set choices. The finite-horizon Gaussian change-of-measure calculation supports later comparisons of adaptive experiments.

A Probabilistic and elimination preliminaries

A.1 Gaussian tails and finite adaptive experiments

  • The finite-horizon Gaussian change-of-measure calculation uses the relative-entropy chain rule for adaptive transcripts, with return treated as absorbing.Source: §A.1 · pp. 13–14
  • Including the algorithm’s seed gives equality; discarding it yields an upper bound, which also applies to mixtures after a common latent variable is discarded.Source: §A.1 · p. 14
  • The comparisons are made at finite horizons before increasing limits of return events are taken.Source: §A.1 · p. 14

A.2 A median-elimination subroutine with a deterministic sample budget

The appendices supply deterministic-budget elimination tools, relate geometrically weighted gap groups to complexity and entropy, and develop a lower bound by comparing the original instance with a two-best-arm experiment.

A.2 A median-elimination subroutine with a deterministic sample budget

  • Median elimination returns an arm within ε of the best with probability at least 1−β and uses a deterministic sample count.Source: §A.2 · p. 14

A.3 Threshold elimination and retention of at least half the arms

  • Threshold elimination retains the best with high probability and, when s>4N, bounds the retained set using the number N of arms within gap d; for s≤4 it can return exactly the best.Source: §A.3 · p. 15

A.4 Geometrically weighted group sizes and their entropy

  • The geometric group construction gives H≤V<8H, and the conditional entropy of auxiliary Z is bounded by the absolute constant C0.Source: §A.4 · p. 16

B A gap-entropy lower bound on the original instance

B.1 Symmetrization and finite transcript experiments

This section develops lower-bound arguments using symmetrization and finite-transcript experiments, alongside successive-run algorithms and analyses of their correctness and expected cost. It also bounds eligible eliminations of near-optimal arms by examining empirical-mean cases and conditional probabilities.

B.1 Symmetrization and finite transcript experiments

  • Random relabeling makes the algorithm permutation-equivariant without changing its permutation-averaged expected stopping time, while finite transcripts support relative-entropy comparisons.For Gaussian observations, each sample from arm i contributes (µ_i − ν_i)^2/2 to the transcript relative entropy.Source: §B.1 · p. 17

B.2 Distributions on the original instance and instances with two best arms

  • The comparison law Q_a is formed by giving label 1 the best mean and removing one gap-a arm, producing an instance with exactly two best arms.The proof perturbs one tied best mean and uses finite-horizon transcript comparisons to bound output probabilities without assuming termination under Q_a.Source: §B.2 · p. 18

B.3 Disjoint stopping events under a common comparison distribution

  • For every gap d, the stopping event E_d has probability greater than 1/2 under P_d, enabling comparisons of many such events under a common Q_a.The construction selects disjoint stopping events on a logarithmic sample-count scale.Source: §B.3 · pp. 19–20

B.4 From scale counting to entropy

  • The entropy argument concludes with coverage of repeated suboptimal means, arbitrary positive gaps, 0 < δ < 1/10, and best mean 1.It obtains Theorem B.1 after undoing symmetrization and taking the infimum over δ-correct algorithms.Source: §B.4 · p. 21

C An instance-wise upper bound

  • For each target instance and 0 < δ < 1/10, a δ-correct algorithm exists with finite expected stopping time on every unique-best input, uniformly over target labelings.The proposition permits construction parameters to depend on the target instance.Source: C An instance-wise upper bound · p. 21

C.1 Parameters and one finite run

  • A single run is finite, returns the correct arm on a target labeling with probability at least 1 − ε, and has incorrect-return probability at most ε on every unique-best input.Its deterministic sample budget is bounded using the fixed target parameters, even when the actual input has different gaps.Source: §C.1 · pp. 22–23

C.2 A finite-expectation fallback

  • The fallback is δ/2-correct and has finite expected sample count on every unique-best input, but requires no sharp instance-dependent guarantee.Its correctness follows from a union bound over arms and rounds when all confidence intervals contain their true means.Source: §C.2 · pp. 23–24

C.3 Correctness on every instance and target expected cost

  • The next construction performs independent runs indexed by t = 0, 1, … .Source: §C.3 · p. 24

L + Ent(I)

  • Interleaving preserves δ-correctness and raises expected cost by at most a factor of two plus one sample, proving Theorem 2.1’s upper-bound direction.The run/fallback construction terminates almost surely on every unique-best input, including instances different from the fixed target.Source: L + Ent(I) · p. 24, §C.3 · p. 24

D A single algorithm

  • The gap-agnostic algorithm runs successive trials using active-set scales, deterministic sample reservations, PAC-selected references, and reused reference estimates within each scale.It receives only the arms and confidence level; instance complexity, gaps, and gap entropy enter only in the analysis.Source: D A single algorithm · p. 25, §D.1 · p. 25

D.2 The procedure and its reservation order

  • Each run reserves the full call budget before sampling, shrinks retained sets, and makes finitely many calls before returning or aborting.Same-scale continuation reduces active-set size by exact halving up to rounding, or by a factor of at most 3/4 when at least three arms remain.Source: §D.2 · p. 26

D.3 Reference estimation and underestimation events

  • Reference upper bounds identify when eliminating a near-optimal arm requires an underestimation event, while fresh Gaussian errors are bounded without conditioning on that reference event.This separation is used in the correctness proof.Source: §D.3 · p. 27

E.1 Stochastic domination for adaptive sampling

  • Adaptive underestimation events across original arms are dominated by independent Bernoulli variables through a common-clock Poisson coupling.The coupling realizes the algorithm’s observation law despite adaptive active sets, scales, and sample counts.Source: §E.1 · pp. 27–28

E Correctness through sets of near-optimal arms

  • The correctness analysis charges underestimations in calls with at most seven arms once and uses a fixed nested family of near-optimal-arm sets for other outputs.The family contains the best arm, has at most one distinct member of each cardinality, and does not grow due to empty gap scales.Source: §E.2 · pp. 28–29, §E.3 · p. 29

E.4 Small and intermediate weight bounds

  • For a fixed near-optimal set, small-budget runs contribute at most Ar, while the intermediate range h/192 < M < h contributes at most 8Ar.The intermediate range contains at most eight dyadic budgets.Source: §E.4 · p. 30

E.5 A bound on eliminating near-optimal arms in one call

  • For large budgets, the analysis bounds eligible calls that eliminate all but at most one near-optimal arm when their reference satisfies the upper bound; if h = 0, such elimination is impossible.The lemma assumes a run of total weight at most M with M ≥ h, and applies to calls with at least eight arms and at least one active arm in the fixed set.Source: §E.5 · pp. 30–31
  • In the complementary case, elimination requires omitting a high-estimate arm in B, while at most one empirical upper-half member is in B and at most s/8 outside arms have true gap below g.The argument then counts upper-half members satisfying (E.15); its count is stronger when q = 1 because no arm in B is retained.Source: §E.5 · p. 31
  • Combining the empirical-mean cases with (E.13) yields a conditional bound for eligible elimination events, using (E.13) alone when x < 2.The argument also establishes that the reference upper bound holds for the eligible event.Source: §E.5 · p. 32
  • Because eligibility is determined before fresh estimates, a union bound over predictable conditional probabilities and the pathwise weight bound controls the occurrence of an eligible event with its reference upper bound holding.The argument does not condition on any future reference upper-bound event.Source: §E.5 · p. 32
  • When h = 0, the elimination event is impossible: all active arms belong to B, and retaining the empirical upper half of at least eight arms keeps at least four in B.Uniqueness of the best arm and positivity of every outside-arm complexity imply there are no outside arms in this case.Source: §E.5 · p. 32

E.6 Large weight bounds and the final error bound

The proof bounds the algorithm’s error and shows how good sample paths ensure large enough runs complete. These controls support correctness and deterministic bounds on the weights of calls.

E.6 Large weight bounds and the final error bound

  • The total incorrect-output probability is bounded to establish δ-correctness, together with almost-sure termination.The proof combines the error bound with the termination result established in Appendix F.Source: §E.6 · p. 33

F Expected sample complexity without instance parameters

  • The sample-complexity analysis uses good sample paths to show that sufficiently large runs succeed with constant probability, while deterministic budgets control other paths.The budget controls include paths on which the best arm is eliminated.Source: F Expected sample complexity without… · p. 33

F.1 A good event in a fresh run

  • On a good path, a fresh run’s modified elimination procedure retains the best arm and makes progress with failure probability bounded per call.The sufficient retention and progress conditions yield a bound below α for their combined conditional failure probability.Source: §F.1 · p. 34

F.2 Deterministic bounds on the weights of calls

  • On a good path, the process finishes by scale K when its weight bound permits the calls; for h_j ≥ H, prospective cumulative weight is below 171H.The proof uses this bound to show no such prefix aborts at the weight bound.Source: §F.2 · p. 34

F.3 Sample complexity on the good event

On good paths, the paper bounds the sample cost of runs using the gap entropy and run scale. It then sums trajectories to show the algorithm terminates almost surely, has finite expected sample count, and needs no instance-specific quantities as input.

F.3 Sample complexity on the good event

  • Only calls with at most seven active arms incur the additional confidence-allocation sample cost; calls with at least eight incur none.At a fixed scale, once call size is at most seven, subsequent call sizes are bounded by 7, 4, and 2.Source: §F.3 · p. 35
  • On a good path, a run’s declared sample cost is bounded in terms of L, Ent(I), and log(h_j/H).The bound applies to complete prospective call reservations, not just samples taken before a sample-budget rejection.Source: §F.3 · p. 35

F.4 Choosing the fixed budget constant and summing all trajectories

  • The algorithm stops almost surely and has finite expected sample count on every instance with a unique best arm.The analysis also establishes that the probability of infinitely many runs is zero.Source: §F.4 · p. 36
  • The quantities used to prove the bound are not inputs to the algorithm.The proof-only quantities include B, H, D, K, W, Ψ, and j*; the theorem’s bound is completed using the error bound from E.6.Source: §F.4 · p. 37

G Consequences and normalization

The results translate the bounds to measurements with known common noise and show when the additive two-arm term is absorbed. They also establish how the lower bound and algorithms extend across several formulations of internal randomness.

G Consequences and normalization

  • After rescaling known common-variance measurements, the complexity depends on squared noise-to-gap ratios, not the origin or units of the scores.Each normalized observation uses exactly one original observation.Source: G Consequences and normalization · p. 37

L + Ent(I)

  • When all suboptimal gaps are equal, Ent(I) = 0 and the two-arm term is absorbed when (n − 1)L ≥ ℓ(D).The common gap need not be known to the procedure.Source: L + Ent(I) · p. 37

H Internal randomness and the scope of the algorithm model

  • The lower-bound result is unchanged for arbitrary standard Borel internal randomness, while the appendix also covers abandonment and probability-kernel formulations.For probability kernels, the result is a lower-bound comparison; equality of the infima is not claimed.Source: H Internal randomness and the scope of… · p. 38, §H.6 · p. 42

H.1 Algorithms with a standard Borel internal random seed; H.2 Representing internal randomness by a Gaussian seed

  • Any standard Borel random seed can be represented by a Gaussian seed while preserving the algorithm’s state-sequence law, success probability, expected sample count, and termination behavior.The representation is measurable; it does not guarantee finite-bit or time-efficient computation.Source: §H.2 · pp. 38–39

H.3 Equality of the instance-wise lower bounds

  • The instance-wise lower bound is equal over Gaussian-seed and arbitrary standard Borel-seed algorithm families.The equality does not require a minimizing algorithm, finite expectation, or termination.Source: §H.3 · pp. 39–40

H.4 The upper-bound algorithms need no internal randomness

  • Both upper-bound algorithms are seed independent and can be implemented using decision functions of the observed history alone.Their correctness and cost bounds are established elsewhere in the appendices.Source: §H.4 · p. 40

H.5 Explicit abandonment

  • Replacing explicit abandonment with a return preserves sampling requests and expected cost while weakly increasing success probability.It does not preserve the complete return law or exact success probability.Source: §H.5 · p. 41

H.6 History-dependent probability kernels

  • History-dependent probability kernels can be implemented with an internal random seed while preserving success probability, expected sample count, and termination behavior.The lower bound applies to their direct costs, but the paper does not claim equality of the kernel and randomized-algorithm infima.Source: §H.6 · pp. 41–42

H.7 The logarithmic convention

The paper uses a positive truncation of the two-arm logarithmic term so it remains defined and nonnegative across admissible gaps. This convention is equivalent up to constants to a positive gap-based expression, while the untruncated display is restricted near the smallest gaps.

H.7 The logarithmic convention

  • For 0 < Δ < 1 the paper uses ℓ(D) = log(e + log(e + D)), with D = Δ^-2, and sets the convention at Δ = 1 to 1.The untruncated expression is negative for e^-1 < Δ < 1 and undefined at Δ = 1.Source: §H.7 · p. 42
  • Across the admissible gap range, the positive conventions ℓ(Δ^-2) and g(Δ) are equivalent up to absolute constants.For small gaps, Δ^-2ℓ(Δ^-2) and Δ^-2 log log(1/Δ) have the same asymptotic order.Source: §H.7 · pp. 42–43
  • The untruncated two-arm display applies on its stated small-gap range, not uniformly near Δ[2] = 1.On the remaining bounded range the corollary states a bound in terms of the instance-wise lower bound alone.Source: §H.7 · p. 43

I Machine-checked verification

The Lean 4 development formalizes the model and verifies the paper’s main statements, alongside results concerning algorithm formulations. The appendix also reports proof-checking audits and clarifies what the formalization does not verify.

I Machine-checked verification

  • The formal model fixes Gaussian rewards, measurable sample-or-return algorithms, and unconditional expected sample counts, with δ-correctness over every admissible instance and arm count.Its definitions and target statements were independently transcribed and checked to coincide with those used in the proofs.Source: I Machine-checked verification · p. 44
  • The Lean development verifies the stated instance-wise lower- and upper-bound results and the guarantee for one algorithm family receiving only δ and n.The verified statements include a bound using the truncated two-arm term and its equivalent g(Δ[2]) form.Source: I Machine-checked verification · p. 44
  • The formal proofs deliberately differ from the appendix presentation, including their lower-bound construction and deterministic-budget algorithm variants.The variants are stated to change only absolute constants and to be covered by the same arguments.Source: I Machine-checked verification · pp. 44–45
  • The development was compiled and kernel-checked with an audit finding no use of sorry, but the informal text was not verified and the work had no outside review.The audit reports only propext, Classical.choice, and Quot.sound as axioms.Source: I Machine-checked verification · p. 45

Related papers

Loading 2609.13703v1…