BanditRLProof.DelayedFeedback.OrderedProcessingTransition

Structural state while Algorithm 5 is processing newly observed feedback before action `currentActionRound`. `processedOrder` is the paper sequence `S`, not a sorted set of source rounds. The current intra-round active set is contained in the previous action round's line-15 active set. Together with the antitone source-round trace, this is the primitive invariant from which a line-7 trace summary obtains current-to-source active persistence.

structure DelayedSAPOStructuralRoundState (K : Nat) where

Every source already in the processed order lies no later than the action round immediately preceding the current one.

theorem source_le_roundStart {K : Nat} (state : DelayedSAPOStructuralRoundState K) {s : Nat} (hs : s ∈ state.processedOrder) : s <= state.currentActionRound - 1

The current intra-round active set is contained in the source-round active set of every previously processed item.

theorem currentActive_subset_activeAtSourceRound {K : Nat} (state : DelayedSAPOStructuralRoundState K) {s : Nat} (hs : s ∈ state.processedOrder) : state.currentActive <= state.activeAtSourceRound s

One source-faithful no-switch iteration of Algorithm 5's inner processing loop. `source_new` is exactly line 3's membership in `B(t) \ S`. The numerical fields are the values read by line 7 after line 4 has appended `sourceRound`; constructing them from observed losses is a separate recursive-state leaf.

structure DelayedSAPONoSwitchProcessOne {K : Nat} (state : DelayedSAPOStructuralRoundState K) where

Algorithm 5 line 4: append the selected source to the end of the processing sequence.

def extendedOrder {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) : List Nat

The line-3 source was not already present in the processed sequence.

theorem sourceRound_not_mem {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) : step.sourceRound ∉ state.processedOrder

Appending one genuinely new source preserves duplicate freedom.

theorem extendedOrder_nodup {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) : step.extendedOrder.Nodup

Every source in the extended sequence satisfies the paper's exact strict availability condition at the current action round.

theorem extendedOrder_available {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) {s : Nat} (hs : s ∈ step.extendedOrder) : s + state.delayAt s < state.currentActionRound

Every source in the extended sequence is at most the previous action round.

theorem extendedSource_le_roundStart {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) {s : Nat} (hs : s ∈ step.extendedOrder) : s <= state.currentActionRound - 1

The line-7 active set is contained in every source-time line-15 active set represented by the extended processing sequence.

theorem currentActive_subset_extendedSourceActive {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) {s : Nat} (hs : s ∈ step.extendedOrder) : state.currentActive <= state.activeAtSourceRound s

Line-7 trace summary after, not before, Algorithm 5 line 4 appends the newly observed source. Its source-index injectivity, strict availability, and current-to-source containment are derived from the ordered transition state.

def toPreEliminationSummary {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) : DelayedSAPOProcessedTraceSummary K where

The exact Algorithm-5 line-8 removal is contained in the active set read by the line-7 snapshot.

theorem line8RemainingActive_subset_currentActive {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) : (step.toPreEliminationSummary.toConfidenceSnapshot horizon).remainingActive <= state.currentActive

Algorithm 5 line 8 successor for the same action round. It preserves the ordered source sequence and updates only the intra-round active set to the exact line-7 complement.

noncomputable def afterLine8 {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) : DelayedSAPOStructuralRoundState K where

Line 8 can only remove arms from the current intra-round active set.

theorem afterLine8_currentActive_subset_before {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) : (step.afterLine8 horizon).currentActive <= state.currentActive

The line-8 successor remains below the active set at the start of the current action round, so another arbitrary new arrival can be processed.

theorem afterLine8_preserves_roundStart {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) : (step.afterLine8 horizon).currentActive <= state.activeAtSourceRound (state.currentActionRound - 1)