BanditRLProof.DelayedFeedback.StochasticGapOrderingAudit

The scalar form of the empirical width printed in the delayed-SAPO source, with `scale = 2 * log T` and `count = n_i(S)`. A nonpositive count uses the capped width `1`; this prevents Lean's totalized real division at zero from manufacturing a zero-width observation. Keeping the scale explicit isolates the positive-count order issue from logarithmic side conditions.

noncomputable def sourceEmpiricalWidthScale (scale count : Real) : Real

For nonnegative scale and positive counts, the source empirical width is antitone in the count. Thus a later state with at least as many pulls has no larger width than an earlier prefix.

theorem sourceEmpiricalWidthScale_antitone (scale countEarlier countLater : Real) (hscale : 0 <= scale) (hcountEarlier : 0 < countEarlier) (hcount : countEarlier <= countLater) : sourceEmpiricalWidthScale scale countLater <= sourceEmpiricalWidthScale scale countEarlier

The small-count branch used in the source proof of Lemma D.10. If the count is at most `96 * scale`, then the capped inverse-square-root width is at least one tenth. For the printed choice `scale = 2 * log T`, this is exactly the implication from `count <= 192 * log T` to `1 <= 10 * width`.

theorem one_le_ten_mul_sourceEmpiricalWidthScale_of_count_le_96_mul_scale (scale count : Real) (hscale : 0 < scale) (hcount : count <= 96 * scale) : 1 <= 10 * sourceEmpiricalWidthScale scale count

Source-parameter specialization of the preceding small-count lemma.

theorem one_le_ten_mul_sourceEmpiricalWidthScale_two_log_of_small_count (horizon count : Real) (hhorizon : 1 < horizon) (hcount : count <= 192 * Real.log horizon) : 1 <= 10 * sourceEmpiricalWidthScale (2 * Real.log horizon) count

Exact small instance used to audit the direction of the displayed D.10 prefix-to-elimination inequality.

theorem sourceEmpiricalWidthScale_one_one : sourceEmpiricalWidthScale 1 1 = 1

Four times the count gives half the uncapped width in the same exact instance.

theorem sourceEmpiricalWidthScale_one_four : sourceEmpiricalWidthScale 1 4 = (1 / 2 : Real)

The reverse inequality used in the displayed D.10 proof is not a generic consequence of prefix count growth: it already fails at scale one between counts one and four. This diagnoses an edge of the frozen proof, not a counterexample to every possible repair of Lemma D.10.

theorem not_sourceEmpiricalWidthScale_one_le_four : not (sourceEmpiricalWidthScale 1 1 <= sourceEmpiricalWidthScale 1 4)

A literal source-width instance at integer horizon `T = 4`. Moving from one to four processed pulls strictly decreases the printed capped radius, so the reverse transport fails inside the paper's own parameter domain rather than only for the normalized scale-one diagnostic above.

theorem not_sourceEmpiricalWidthScale_horizon_four_one_le_four : ¬ (sourceEmpiricalWidthScale (2 * Real.log 4) 1 <= sourceEmpiricalWidthScale (2 * Real.log 4) 4)

At one source elimination snapshot, the line-7 strict test and the elimination projection of the stochastic good event put the eliminated arm's true gap strictly above eight empirical widths. This is the lower endpoint used by the repaired D.12 route below; it is derived from the actual source snapshot rather than supplied as a scalar contract field.

theorem eight_mul_empiricalWidth_lt_gap_of_mem_eliminated {K : Nat} [Nonempty (Fin K)] (snapshot : DelayedSAPOSourceConfidenceSnapshot K) (mean : Fin K -> Real) (optimal i : Fin K) (hoptimal : forall j, mean optimal <= mean j) (hgood : snapshot.EliminationGoodEvent mean) (hi : i ∈ snapshot.eliminated) : 8 * snapshot.empiricalWidth i < mean i - mean optimal

A still-active arm's gap is at most sixteen of its widths at the same processed prefix, once the source upper-confidence surface is bounded by the current optimal-arm empirical radius and the optimal width is within factor three. These are exactly the algebraic facts used inside the displayed D.10 proof; no transport to a later elimination prefix occurs here.

theorem gap_le_sixteen_mul_empiricalWidth_of_mem_remainingActive {K : Nat} [Nonempty (Fin K)] (snapshot : DelayedSAPOSourceConfidenceSnapshot K) (mean : Fin K -> Real) (optimal i : Fin K) (hgood : snapshot.EliminationGoodEvent mean) (hi : i ∈ snapshot.remainingActive) (hucbCurrent : snapshot.ucbStar <= snapshot.empiricalMean optimal + snapshot.empiricalWidth optimal) (hoptimalWidth : snapshot.empiricalWidth optimal <= 3 * snapshot.empiricalWidth i) : mean i - mean optimal <= 16 * snapshot.empiricalWidth i

Source-faithful case split behind the D.10 active-arm upper endpoint. The large-count branch supplies the current-UCB and factor-three width edges. The small-count branch supplies the printed width formula together with `count <= 96 * scale`; bounded losses then give `gap <= 1 <= 10 * width`. This removes the unconditional factor-three assumption from the combined consumer while leaving the recursive count and width-shape producers explicit.

theorem gap_le_sixteen_mul_empiricalWidth_of_mem_remainingActive_of_large_or_small_count {K : Nat} [Nonempty (Fin K)] (snapshot : DelayedSAPOSourceConfidenceSnapshot K) (mean : Fin K -> Real) (optimal i : Fin K) (hmeanBounds : forall j, mean j ∈ Set.Icc (0 : Real) 1) (hgood : snapshot.EliminationGoodEvent mean) (hi : i ∈ snapshot.remainingActive) (hbranch : (snapshot.ucbStar <= snapshot.empiricalMean optimal + snapshot.empiricalWidth optimal /\ snapshot.empiricalWidth optimal <= 3 * snapshot.empiricalWidth i) \/ (exists scale count : Real, 0 < scale /\ count <= 96 * scale /\ snapshot.empiricalWidth i = sourceEmpiricalWidthScale scale count)) : mean i - mean optimal <= 16 * snapshot.empiricalWidth i

Same-snapshot repair of the displayed D.12 / main-text Lemma 4.2 chain. When `iEarlier` is eliminated and `iLater` remains active in that very update, the active-prefix D.10 gap upper bound can be consumed before any later elimination snapshot is mentioned. The proof therefore avoids the reversed prefix-to-elimination width inequality diagnosed above. The two width comparison premises still have to be produced by the source count event on a recursive Delayed SAPO trajectory.

theorem gap_le_twenty_mul_gap_at_earlier_elimination_snapshot {K : Nat} [Nonempty (Fin K)] (snapshot : DelayedSAPOSourceConfidenceSnapshot K) (mean : Fin K -> Real) (optimal iEarlier iLater : Fin K) (hoptimal : forall j, mean optimal <= mean j) (hgood : snapshot.EliminationGoodEvent mean) (hEarlierEliminated : iEarlier ∈ snapshot.eliminated) (hLaterRemaining : iLater ∈ snapshot.remainingActive) (hucbCurrent : snapshot.ucbStar <= snapshot.empiricalMean optimal + snapshot.empiricalWidth optimal) (hoptimalWidth : snapshot.empiricalWidth optimal <= 3 * snapshot.empiricalWidth iLater) (hpairWidth : snapshot.empiricalWidth iLater <= 10 * snapshot.empiricalWidth iEarlier) : mean iLater - mean optimal <= 20 * (mean iEarlier - mean optimal)

The same-snapshot factor-twenty consumer with the source's large/small- count split exposed. In the small-count branch the factor-three premise is replaced by bounded means and the exact source-width lower bound. The theorem still requires a recursive producer for the selected branch and the same- prefix factor-ten comparison; it is not an unconditional port of D.10/D.12.

theorem gap_le_twenty_mul_gap_at_earlier_elimination_snapshot_of_large_or_small_count {K : Nat} [Nonempty (Fin K)] (snapshot : DelayedSAPOSourceConfidenceSnapshot K) (mean : Fin K -> Real) (optimal iEarlier iLater : Fin K) (hoptimal : forall j, mean optimal <= mean j) (hmeanBounds : forall j, mean j ∈ Set.Icc (0 : Real) 1) (hgood : snapshot.EliminationGoodEvent mean) (hEarlierEliminated : iEarlier ∈ snapshot.eliminated) (hLaterRemaining : iLater ∈ snapshot.remainingActive) (hbranch : (snapshot.ucbStar <= snapshot.empiricalMean optimal + snapshot.empiricalWidth optimal /\ snapshot.empiricalWidth optimal <= 3 * snapshot.empiricalWidth iLater) \/ (exists scale count : Real, 0 < scale /\ count <= 96 * scale /\ snapshot.empiricalWidth iLater = sourceEmpiricalWidthScale scale count)) (hpairWidth : snapshot.empiricalWidth iLater <= 10 * snapshot.empiricalWidth iEarlier) : mean iLater - mean optimal <= 20 * (mean iEarlier - mean optimal)

Exact deterministic interface needed by the displayed proof of source Lemma D.12 (main-text Lemma 4.2). Its index is a shared processed-sequence prefix length, not wall-clock action time. The fields deliberately name the four edges consumed by D.12: D.10 supplies the gap endpoints and cross-arm comparison, while the width definition supplies the time transport.

structure DelayedSAPOD10D12GapOrderingContract (K : Nat) where

The source surrogate gap `Delta-tilde_i = 8 width_i(S-tilde_i)`.

noncomputable def surrogateGap {K : Nat} (contract : DelayedSAPOD10D12GapOrderingContract K) (i : Fin K) : Real

Lower half of the displayed D.10 two-sided surrogate-gap comparison.

theorem surrogateGap_le_gap {K : Nat} (contract : DelayedSAPOD10D12GapOrderingContract K) (i : Fin K) : contract.surrogateGap i <= contract.gap i

Upper half of the displayed D.10 two-sided comparison, exposed from the factor-16 endpoint rather than assumed in factor-two form.

theorem gap_le_two_mul_surrogateGap {K : Nat} (contract : DelayedSAPOD10D12GapOrderingContract K) (i : Fin K) : contract.gap i <= 2 * contract.surrogateGap i

The four inequalities in the source's displayed D.12 chain, kept separate so an audit can identify which edge is missing from a recursive Delayed SAPO implementation.

theorem d12_gap_ordering_chain {K : Nat} (contract : DelayedSAPOD10D12GapOrderingContract K) (iEarlier iLater : Fin K) (horder : contract.eliminationPrefixIndex iEarlier <= contract.eliminationPrefixIndex iLater) : contract.gap iLater <= 16 * contract.widthAt iLater (contract.eliminationPrefixIndex iLater) /\ 16 * contract.widthAt iLater (contract.eliminationPrefixIndex iLater) <= 16 * contract.widthAt iLater (contract.eliminationPrefixIndex iEarlier) /\ 16 * contract.widthAt iLater (contract.eliminationPrefixIndex iEarlier) <= 160 * contract.widthAt iEarlier (contract.eliminationPrefixIndex iEarlier) /\ 160 * contract.widthAt iEarlier (contract.eliminationPrefixIndex iEarlier) <= 20 * contract.gap iEarlier

Conditional source Lemma D.12 / main-text Lemma 4.2 consumer. It proves the factor-20 gap ordering once the exact D.10 endpoints and the correctly oriented width transport are supplied; it does not claim those disputed inputs follow from the current one-snapshot library.

theorem gap_le_twenty_mul_gap_of_eliminationPrefixIndex_le {K : Nat} (contract : DelayedSAPOD10D12GapOrderingContract K) (iEarlier iLater : Fin K) (horder : contract.eliminationPrefixIndex iEarlier <= contract.eliminationPrefixIndex iLater) : contract.gap iLater <= 20 * contract.gap iEarlier