BanditRLProof.DelayedFeedback.EliminatedArmInitialization

Algorithm 5 line 10's initial sampling probability `p_i^1 = 1/(2K) + n_i(S)/(2T)`.

noncomputable def delayedSAPOInitialEliminatedProbability (armCount horizon pullCount : Nat) : Real

Algorithm 5 line 10's first EAP phase target `N_i^1 = 1280/(p_i^1 * (Delta-tilde_i)^2)`.

noncomputable def delayedSAPOInitialPhaseTarget (probability surrogateGap : Real) : Real

A positive source scale makes the capped inverse-square-root width strictly positive, including the zero-count branch where the width is one.

theorem sourceEmpiricalWidthScale_pos (scale count : Real) (hscale : 0 < scale) : 0 < sourceEmpiricalWidthScale scale count

Per-arm data created by Algorithm 5 line 10. `processedAtProbabilityLevel j` represents the source sets `C_i^(p_i^1 * 2^(-j))`; line 10 initializes every represented level to the empty set. Later EAP calls and their phase transitions remain a separate state-machine leaf.

structure DelayedSAPOEliminatedArmInitialization (K : Nat) where

Registry of EAP data. Active arms have not yet entered EAP and are therefore represented by `none`.

abbrev DelayedSAPOEliminatedArmBank (K : Nat)

Round-start invariant needed to justify that line 10 initializes rather than resets every arm in the newly eliminated set.

def ActiveArmsUninitialized {K : Nat} (state : DelayedSAPOStructuralRoundState K) (bank : DelayedSAPOEliminatedArmBank K) : Prop

Construct exactly the line-10 data for one candidate arm from the post-line-4 numerical snapshot. Membership in the line-7 elimination set is enforced by `initializeIfEliminated` below.

noncomputable def ofProcessOne {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) : DelayedSAPOEliminatedArmInitialization K

Algorithm 5 lines 9--10 initialize precisely the arms selected by the line-7 elimination set. Returning `Option` keeps that domain visible instead of silently producing EAP state for an arm that remains active.

noncomputable def initializeIfEliminated {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) : Option (DelayedSAPOEliminatedArmInitialization K)

Pointwise line-10 update of an existing EAP registry. Arms in the new line-7 elimination set receive the literal source initializer; every other arm keeps its prior state.

noncomputable def initializeNewlyEliminated {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (prior : DelayedSAPOEliminatedArmBank K) : DelayedSAPOEliminatedArmBank K

No declaration docstring is present; use the chapter context and exact statement below.

theorem initializeIfEliminated_eq_some_iff {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) : initializeIfEliminated step horizon i = some (ofProcessOne step horizon i) <-> i ∈ (step.toPreEliminationSummary.toConfidenceSnapshot horizon).eliminated

No declaration docstring is present; use the chapter context and exact statement below.

theorem initializeIfEliminated_eq_none_iff {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) : initializeIfEliminated step horizon i = none <-> i ∉ (step.toPreEliminationSummary.toConfidenceSnapshot horizon).eliminated

No declaration docstring is present; use the chapter context and exact statement below.

theorem initializeNewlyEliminated_of_mem {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (prior : Fin K -> Option (DelayedSAPOEliminatedArmInitialization K)) (i : Fin K) (hi : i ∈ (step.toPreEliminationSummary.toConfidenceSnapshot horizon).eliminated) : initializeNewlyEliminated step horizon prior i = some (ofProcessOne step horizon i)

No declaration docstring is present; use the chapter context and exact statement below.

theorem initializeNewlyEliminated_of_not_mem {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (prior : Fin K -> Option (DelayedSAPOEliminatedArmInitialization K)) (i : Fin K) (hi : i ∉ (step.toPreEliminationSummary.toConfidenceSnapshot horizon).eliminated) : initializeNewlyEliminated step horizon prior i = prior i

Line 10 can change an arm's EAP-bank entry only when line 7 selected that arm for elimination in the same snapshot.

theorem mem_eliminated_of_initializeNewlyEliminated_ne_prior {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (prior : Fin K -> Option (DelayedSAPOEliminatedArmInitialization K)) (i : Fin K) (hchanged : initializeNewlyEliminated step horizon prior i ≠ prior i) : i ∈ (step.toPreEliminationSummary.toConfidenceSnapshot horizon).eliminated

An arm that remains active after line 8 is not reset by line 10.

theorem initializeNewlyEliminated_eq_prior_of_mem_remainingActive {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (prior : Fin K -> Option (DelayedSAPOEliminatedArmInitialization K)) (i : Fin K) (hi : i ∈ (step.toPreEliminationSummary.toConfidenceSnapshot horizon).remainingActive) : initializeNewlyEliminated step horizon prior i = prior i

Every arm selected by line 7 was active immediately before line 8, so a valid prior bank has no EAP state for it yet.

theorem prior_eq_none_of_mem_eliminated {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (prior : DelayedSAPOEliminatedArmBank K) (hprior : ActiveArmsUninitialized state prior) (i : Fin K) (hi : i ∈ (step.toPreEliminationSummary.toConfidenceSnapshot horizon).eliminated) : prior i = none

After line 10, every arm that survives line 8 is still uninitialized in the EAP bank.

theorem remainingActive_uninitialized_after_initialize {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (prior : DelayedSAPOEliminatedArmBank K) (hprior : ActiveArmsUninitialized state prior) (i : Fin K) (hi : i ∈ (step.toPreEliminationSummary.toConfidenceSnapshot horizon).remainingActive) : initializeNewlyEliminated step horizon prior i = none

No declaration docstring is present; use the chapter context and exact statement below.

theorem ofProcessOne_arm {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) : (ofProcessOne step horizon i).arm = i

No declaration docstring is present; use the chapter context and exact statement below.

theorem ofProcessOne_eliminationRound {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) : (ofProcessOne step horizon i).eliminationRound = state.currentActionRound

No declaration docstring is present; use the chapter context and exact statement below.

theorem ofProcessOne_eliminationProcessedOrder {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) : (ofProcessOne step horizon i).eliminationProcessedOrder = step.extendedOrder

No declaration docstring is present; use the chapter context and exact statement below.

theorem ofProcessOne_errorCount {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) : (ofProcessOne step horizon i).errorCount = 0

No declaration docstring is present; use the chapter context and exact statement below.

theorem ofProcessOne_phaseIndex {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) : (ofProcessOne step horizon i).phaseIndex = 1

No declaration docstring is present; use the chapter context and exact statement below.

theorem ofProcessOne_phaseSamples {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) : (ofProcessOne step horizon i).phaseSamples = []

No declaration docstring is present; use the chapter context and exact statement below.

theorem ofProcessOne_processedAtProbabilityLevel {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) (j : Nat) : (ofProcessOne step horizon i).processedAtProbabilityLevel j = {}

The source initial eliminated-arm probability is strictly positive when there is an arm and the horizon is positive. No count upper bound is needed for this lower endpoint.

theorem initialProbability_pos {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) : 0 < (ofProcessOne step horizon i).initialProbability

With the source-side count bound `n_i(S) <= T`, the initial probability is at most one. The count bound will be generated by the full Algorithm-5 trajectory; it is not manufactured by this numerical initializer.

theorem initialProbability_le_one {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) (hhorizon : 0 < horizon) (hcount : step.toPreEliminationSummary.toProcessedPrefix.processedPullCount i <= horizon) : (ofProcessOne step horizon i).initialProbability <= 1

The line-10 surrogate gap is nonnegative because the exact source width is capped below by zero.

theorem surrogateGap_nonneg {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) : 0 <= (ofProcessOne step horizon i).surrogateGap

For the nontrivial source regime `1 < T`, the frozen line-10 surrogate gap is strictly positive for every processed count.

theorem surrogateGap_pos {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) (hhorizon : 1 < horizon) : 0 < (ofProcessOne step horizon i).surrogateGap

The first EAP phase target is nonnegative without hiding Lean's totalized-division boundary.

theorem initialPhaseTarget_nonneg {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) : 0 <= (ofProcessOne step horizon i).initialPhaseTarget

Under the explicit positive-width condition used by the source analysis, the first EAP phase target has a genuinely positive denominator and value.

theorem initialPhaseTarget_pos {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (i : Fin K) (hhorizon : 1 < horizon) : 0 < (ofProcessOne step horizon i).initialPhaseTarget

Bundled deterministic producer for the next EAP leaf: a newly eliminated arm receives a source-exact state with positive sampling probability, surrogate gap, and first phase target in the nontrivial horizon regime.

theorem initializeNewlyEliminated_spec_of_mem {K : Nat} {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) (horizon : Nat) (hhorizon : 1 < horizon) (prior : Fin K -> Option (DelayedSAPOEliminatedArmInitialization K)) (i : Fin K) (hi : i ∈ (step.toPreEliminationSummary.toConfidenceSnapshot horizon).eliminated) : initializeNewlyEliminated step horizon prior i = some (ofProcessOne step horizon i) ∧ 0 < (ofProcessOne step horizon i).initialProbability ∧ 0 < (ofProcessOne step horizon i).surrogateGap ∧ 0 < (ofProcessOne step horizon i).initialPhaseTarget