BanditRLProof.DelayedFeedback.ProcessedPrefixCounts

A ledger for one ordered ledger of source rounds whose feedback has been processed by delayed SAPO. Each entry stores the arm chosen at that source round and the Algorithm-5 allocation that was in force when the action was sampled. In particular, `inactiveProbabilityAtSource` is source-time data; it must not be reconstructed from the later processing-time state.

structure DelayedSAPOProcessedPrefix (K : Nat) where

The source count `n_i(S)` on the processed ledger.

def processedPullCount {K : Nat} (ledger : DelayedSAPOProcessedPrefix K) (i : Fin K) : Nat

The source conditional mass `sum_{s in S} p_i(s)` on the same ledger.

noncomputable def expectedPullMass {K : Nat} (ledger : DelayedSAPOProcessedPrefix K) (i : Fin K) : Real

Two arms that were active at every source round represented by the processed ledger receive the same cumulative Algorithm-5 probability mass. This is the deterministic line-15 producer used by the D.1 count clause.

theorem expectedPullMass_eq_of_active_throughout {K : Nat} (ledger : DelayedSAPOProcessedPrefix K) (i j : Fin K) (hi : forall s, i ∈ ledger.activeAtSource s) (hj : forall s, j ∈ ledger.activeAtSource s) : ledger.expectedPullMass i = ledger.expectedPullMass j

The exact deterministic projection needed from Algorithm 5 and the pull-count clause of source Definition D.1 at one processed ledger. The certificate keeps the source-time allocation ledger explicit. It assumes the D.1 count inequalities and the source definitions of the width and the recursive empirical UCB, but it does not assume either of the width-comparison conclusions that it is designed to prove. Constructing this projection from the full recursive delayed-SAPO state and proving its probability are separate obligations.

structure DelayedSAPOProcessedPrefixCountCertificate {K : Nat} [Nonempty (Fin K)] (snapshot : DelayedSAPOSourceConfidenceSnapshot K) (ledger : DelayedSAPOProcessedPrefix K) (horizon : Nat) : Prop where

The capped source empirical width is always nonnegative.

theorem sourceEmpiricalWidthScale_nonneg (scale count : Real) : 0 <= sourceEmpiricalWidthScale scale count

The capped source empirical width is at most one.

theorem sourceEmpiricalWidthScale_le_one (scale count : Real) : sourceEmpiricalWidthScale scale count <= 1

If one positive count is at most eight times another, then the other arm's inverse-square-root width is at most three times the reference width. The factor three is the integer relaxation of `sqrt 8` used in source D.10.

theorem sourceEmpiricalWidthScale_le_three_of_count_le_eight_mul (scale countReference countOther : Real) (hscale : 0 <= scale) (hreference : 0 < countReference) (hcount : countReference <= 8 * countOther) : sourceEmpiricalWidthScale scale countOther <= 3 * sourceEmpiricalWidthScale scale countReference

Active arms have equal source-time expected pull mass on the ledger.

theorem expectedPullMass_eq_of_mem_active {K : Nat} [Nonempty (Fin K)] {snapshot : DelayedSAPOSourceConfidenceSnapshot K} {ledger : DelayedSAPOProcessedPrefix K} {horizon : Nat} (certificate : DelayedSAPOProcessedPrefixCountCertificate snapshot ledger horizon) {i j : Fin K} (hi : i ∈ snapshot.active) (hj : j ∈ snapshot.active) : ledger.expectedPullMass i = ledger.expectedPullMass j

Combining the two exact D.1 count inequalities with equal active-arm probability mass gives the stronger `n_j >= n_i/4 - 6 log T` comparison.

theorem quarter_count_sub_six_log_le_count_of_mem_active {K : Nat} [Nonempty (Fin K)] {snapshot : DelayedSAPOSourceConfidenceSnapshot K} {ledger : DelayedSAPOProcessedPrefix K} {horizon : Nat} (certificate : DelayedSAPOProcessedPrefixCountCertificate snapshot ledger horizon) {i j : Fin K} (hi : i ∈ snapshot.active) (hj : j ∈ snapshot.active) : (ledger.processedPullCount i : Real) / 4 - 6 * Real.log (horizon : Real) <= (ledger.processedPullCount j : Real)

In the source large-count branch, any other active arm has at least one eighth of the reference arm's processed count.

theorem eighth_count_le_count_of_large_count {K : Nat} [Nonempty (Fin K)] {snapshot : DelayedSAPOSourceConfidenceSnapshot K} {ledger : DelayedSAPOProcessedPrefix K} {horizon : Nat} (certificate : DelayedSAPOProcessedPrefixCountCertificate snapshot ledger horizon) (hhorizon : 1 < horizon) {i j : Fin K} (hi : i ∈ snapshot.active) (hj : j ∈ snapshot.active) (hlarge : 192 * Real.log (horizon : Real) < (ledger.processedPullCount i : Real)) : (ledger.processedPullCount i : Real) / 8 <= (ledger.processedPullCount j : Real)

The source D.10 factor-three width producer in the large-count branch.

theorem empiricalWidth_le_three_of_large_count {K : Nat} [Nonempty (Fin K)] {snapshot : DelayedSAPOSourceConfidenceSnapshot K} {ledger : DelayedSAPOProcessedPrefix K} {horizon : Nat} (certificate : DelayedSAPOProcessedPrefixCountCertificate snapshot ledger horizon) (hhorizon : 1 < horizon) {iReference iOther : Fin K} (hreferenceActive : iReference ∈ snapshot.active) (hotherActive : iOther ∈ snapshot.active) (hlarge : 192 * Real.log (horizon : Real) < (ledger.processedPullCount iReference : Real)) : snapshot.empiricalWidth iOther <= 3 * snapshot.empiricalWidth iReference

The unconditional same-ledger D.10 width comparison. It is derived from the source-time allocation ledger, the D.1 count event, and the exact source width formula; no factor-ten comparison is assumed as a contract field.

theorem empiricalWidth_le_ten_of_mem_active {K : Nat} [Nonempty (Fin K)] {snapshot : DelayedSAPOSourceConfidenceSnapshot K} {ledger : DelayedSAPOProcessedPrefix K} {horizon : Nat} (certificate : DelayedSAPOProcessedPrefixCountCertificate snapshot ledger horizon) (hhorizon : 1 < horizon) {iReference iOther : Fin K} (hreferenceActive : iReference ∈ snapshot.active) (hotherActive : iOther ∈ snapshot.active) : snapshot.empiricalWidth iOther <= 10 * snapshot.empiricalWidth iReference

The recursive empirical UCB is no larger than the current empirical mean-plus-width surface, so the source minimum `ucbStar` has the current-UCB upper edge needed by the active-arm gap proof.

theorem ucbStar_le_empiricalMean_add_width {K : Nat} [Nonempty (Fin K)] {snapshot : DelayedSAPOSourceConfidenceSnapshot K} {ledger : DelayedSAPOProcessedPrefix K} {horizon : Nat} (certificate : DelayedSAPOProcessedPrefixCountCertificate snapshot ledger horizon) (mean : Fin K -> Real) (hgood : snapshot.EliminationGoodEvent mean) (i : Fin K) : snapshot.ucbStar <= snapshot.empiricalMean i + snapshot.empiricalWidth i

The exact large/small branch expected by the existing active-arm gap consumer is now produced from the processed-ledger certificate.

theorem activeArmGapBranch {K : Nat} [Nonempty (Fin K)] {snapshot : DelayedSAPOSourceConfidenceSnapshot K} {ledger : DelayedSAPOProcessedPrefix K} {horizon : Nat} (certificate : DelayedSAPOProcessedPrefixCountCertificate snapshot ledger horizon) (hhorizon : 1 < horizon) (mean : Fin K -> Real) (hgood : snapshot.EliminationGoodEvent mean) {optimal i : Fin K} (hoptimalActive : optimal ∈ snapshot.active) (hiActive : i ∈ snapshot.active) : (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)

Repaired same-snapshot D.12 / main-text Lemma-4.2 deterministic slice. The theorem removes the manually supplied branch and pair-width premises from the earlier consumer: both are generated by the actual Algorithm-5 source-time allocation ledger and the D.1 count clause. The full recursive state projection and probability of the source good event remain open.

theorem gap_le_twenty_mul_gap_at_earlier_elimination_snapshot_of_countCertificate {K : Nat} [Nonempty (Fin K)] (snapshot : DelayedSAPOSourceConfidenceSnapshot K) (ledger : DelayedSAPOProcessedPrefix K) (horizon : Nat) (certificate : DelayedSAPOProcessedPrefixCountCertificate snapshot ledger horizon) (hhorizon : 1 < horizon) (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) (hoptimalActive : optimal ∈ snapshot.active) (hEarlierEliminated : iEarlier ∈ snapshot.eliminated) (hLaterRemaining : iLater ∈ snapshot.remainingActive) : mean iLater - mean optimal <= 20 * (mean iEarlier - mean optimal)