BanditRLProof.DelayedFeedback.OrderedNoSwitchTrace

Certificate that the no-switch inner loop for one action round is exhausted and that its final intra-round active set is the line-15 active set recorded by the source-round trace. The second field is a structural consistency contract. It is not a claim that EAP has already constructed a valid probability vector.

structure DelayedSAPONoSwitchRoundClose {K : Nat} (state : DelayedSAPOStructuralRoundState K) : Prop where

Exhausting `B(t) \ S` means that the ordered ledger contains exactly the feedback available before action `t`. The equality is set-level only and does not impose a chronological order on simultaneous arrivals.

theorem processedOrder_toFinset_eq_observedBefore {K : Nat} {state : DelayedSAPOStructuralRoundState K} (closed : DelayedSAPONoSwitchRoundClose state) : state.processedOrder.toFinset = observedBefore state.delayAt state.currentActionRound

Structural state at the start of the next action round. The processed ledger and active set are unchanged; the round-start invariant follows from the close certificate's identification with the just-finished source-round active set.

def nextRoundState {K : Nat} {state : DelayedSAPOStructuralRoundState K} (closed : DelayedSAPONoSwitchRoundClose state) : DelayedSAPOStructuralRoundState K where

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

theorem nextRoundState_currentActionRound {K : Nat} {state : DelayedSAPOStructuralRoundState K} (closed : DelayedSAPONoSwitchRoundClose state) : closed.nextRoundState.currentActionRound = state.currentActionRound + 1

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

theorem nextRoundState_processedOrder {K : Nat} {state : DelayedSAPOStructuralRoundState K} (closed : DelayedSAPONoSwitchRoundClose state) : closed.nextRoundState.processedOrder = state.processedOrder

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

theorem nextRoundState_currentActive {K : Nat} {state : DelayedSAPOStructuralRoundState K} (closed : DelayedSAPONoSwitchRoundClose state) : closed.nextRoundState.currentActive = state.currentActive

One edge of the deterministic no-switch structural trace. Processing uses the exact line-8 successor; advancing rounds requires an exhausted-loop certificate.

inductive DelayedSAPONoSwitchStructuralStep {K : Nat} (horizon : Nat) : DelayedSAPOStructuralRoundState K → DelayedSAPOStructuralRoundState K → Prop | process {state : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchProcessOne state) : DelayedSAPONoSwitchStructuralStep horizon state (step.afterLine8 horizon) | nextRound {state : DelayedSAPOStructuralRoundState K} (closed : DelayedSAPONoSwitchRoundClose state) : DelayedSAPONoSwitchStructuralStep horizon state closed.nextRoundState /-- Finite reflexive-transitive no-switch reachability. It is a structural relation, not a generated stochastic trajectory. -/ abbrev DelayedSAPONoSwitchStructuralReachable {K : Nat} (horizon : Nat)

Finite reflexive-transitive no-switch reachability. It is a structural relation, not a generated stochastic trajectory.

abbrev DelayedSAPONoSwitchStructuralReachable {K : Nat} (horizon : Nat)

Every primitive no-switch structural edge can only remove arms.

theorem currentActive_subset_of_structuralStep {K horizon : Nat} {initial final : DelayedSAPOStructuralRoundState K} (step : DelayedSAPONoSwitchStructuralStep horizon initial final) : final.currentActive <= initial.currentActive

Active sets are antitone along every finite no-switch structural trace.

theorem currentActive_subset_of_structuralReachable {K horizon : Nat} {initial final : DelayedSAPOStructuralRoundState K} (run : DelayedSAPONoSwitchStructuralReachable horizon initial final) : final.currentActive <= initial.currentActive

An arm eliminated by a later processing step was still present after an earlier line-8 removal whenever the two steps are connected by a no-switch structural trace. This is the temporal premise previously left to callers.

theorem mem_earlierRemainingActive_of_laterEliminated {K horizon : Nat} {initial laterState : DelayedSAPOStructuralRoundState K} (earlierStep : DelayedSAPONoSwitchProcessOne initial) (between : DelayedSAPONoSwitchStructuralReachable horizon (earlierStep.afterLine8 horizon) laterState) (laterStep : DelayedSAPONoSwitchProcessOne laterState) (iLater : Fin K) (hLaterEliminated : iLater ∈ (laterStep.toPreEliminationSummary.toConfidenceSnapshot horizon).eliminated) : iLater ∈ (earlierStep.toPreEliminationSummary.toConfidenceSnapshot horizon).remainingActive

Ordered two-elimination factor-20 consumer. Unlike the one-snapshot consumer, this theorem derives later-arm survival at the earlier snapshot from the exact structural trace. It remains conditional on the earlier D.4 count clause and elimination-good projection.

theorem gap_le_twenty_mul_gap_of_ordered_no_switch_eliminations {K : Nat} [Nonempty (Fin K)] {initial laterState : DelayedSAPOStructuralRoundState K} (horizon : Nat) (hhorizon : 1 < horizon) (earlierStep : DelayedSAPONoSwitchProcessOne initial) (between : DelayedSAPONoSwitchStructuralReachable horizon (earlierStep.afterLine8 horizon) laterState) (laterStep : DelayedSAPONoSwitchProcessOne laterState) (mean : Fin K → Real) (optimal iEarlier iLater : Fin K) (hoptimal : ∀ i, mean optimal <= mean i) (hmeanBounds : ∀ i, mean i ∈ Set.Icc (0 : Real) 1) (hD4 : earlierStep.toPreEliminationSummary.D4CountClause horizon) (hgood : (earlierStep.toPreEliminationSummary.toConfidenceSnapshot horizon).EliminationGoodEvent mean) (hoptimalActive : optimal ∈ initial.currentActive) (hEarlierEliminated : iEarlier ∈ (earlierStep.toPreEliminationSummary.toConfidenceSnapshot horizon).eliminated) (hLaterEliminated : iLater ∈ (laterStep.toPreEliminationSummary.toConfidenceSnapshot horizon).eliminated) : mean iLater - mean optimal <= 20 * (mean iEarlier - mean optimal)