Replay.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Deterministic virtual-prefix replay for the secretary transport

The prefix is observed and rejected, but its history is retained when the hidden rule is run on the suffix. The following lemmas are pointwise in the complete seed and order; no independence of the suffix order is assumed.

Source: sections/secretary.tex, the paragraph beginning "Initialize the hidden-weight rule". These are supporting transport lemmas, not a proof of the random-prefix law or of the complete secretary endpoint.

def OAI.MatroidProphet.SecretaryReplay.prefixSet line 23
Source documentation
Labels in the first K positions of an arrival order. This also handles K = 0 and K ≥ n without a special convention.
```
def prefixSet {n : ℕ} (π : ArrivalOrder n) (K : ℕ) : Finset (Fin n) :=
…
```
Mentions: OAI.MatroidProphet.ArrivalOrder
theorem OAI.MatroidProphet.SecretaryReplay.mem_prefixSet line 26
def OAI.MatroidProphet.SecretaryReplay.prefixReplay line 33
Source documentation
Replay every observed arrival in the core history, while forcibly rejecting all positions strictly before K. At suffix arrivals the complete past history (including the rejected prefix) is supplied, never a future weight.
```
noncomputable def prefixReplay {n bits : ℕ} (A : HiddenRule n bits) (K : ℕ) :
    OnlineRule n bits where
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.OnlineRule
theorem OAI.MatroidProphet.SecretaryReplay.acceptedThrough_prefixReplay line 44
Source documentation
Prefix rejection removes exactly the prefix labels from the simulated run.
```
theorem acceptedThrough_prefixReplay {n bits : ℕ} (A : HiddenRule n bits) (K : ℕ)
    (r : Seed bits) (s v : Weights n) (π : ArrivalOrder n) (t : ℕ) :
    acceptedThrough (prefixReplay A K) r s v π t =
      acceptedThrough (sampleSimulation A) r s v π t \ prefixSet π K := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.acceptedThrough, OAI.MatroidProphet.SecretaryReplay.prefixReplay, OAI.MatroidProphet.sampleSimulation, OAI.MatroidProphet.SecretaryReplay.prefixSet
theorem OAI.MatroidProphet.SecretaryReplay.acceptedThrough_eq_hidden line 58
Source documentation
If the observed prefix is sacrificed by the hidden rule, explicit prefix rejection changes no accepted label, at any arrival prefix.
```
theorem acceptedThrough_eq_hidden {n bits : ℕ} (A : HiddenRule n bits) (K : ℕ)
    (r : Seed bits) (s v : Weights n) (π : ArrivalOrder n) (t : ℕ)
    (hprefix : prefixSet π K ⊆ A.mask r) :
    acceptedThrough (prefixReplay A K) r s v π t =
      hiddenAcceptedThrough A r (glue (A.mask r) s v) π t := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.SecretaryReplay.prefixSet, OAI.MatroidProphet.acceptedThrough, OAI.MatroidProphet.SecretaryReplay.prefixReplay, OAI.MatroidProphet.hiddenAcceptedThrough, OAI.MatroidProphet.glue
theorem OAI.MatroidProphet.SecretaryReplay.glue_eq_of_agrees line 75
Source documentation
Only agreement on the revealed mask is required of the initial observation.
```
theorem glue_eq_of_agrees {n bits : ℕ} (A : HiddenRule n bits) (r : Seed bits)
    (s w : Weights n) (hobs : ∀ e ∈ A.mask r, s e = w e) :
    glue (A.mask r) s w = w := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.glue
theorem OAI.MatroidProphet.SecretaryReplay.fixedVector_acceptedThrough line 85
Source documentation
Exact virtual replay, with equality at every prefix, not just equal reward.
```
theorem fixedVector_acceptedThrough {n bits : ℕ} (A : HiddenRule n bits) (K : ℕ)
    (r : Seed bits) (s w : Weights n) (π : ArrivalOrder n) (t : ℕ)
    (hprefix : prefixSet π K ⊆ A.mask r)
    (hobs : ∀ e ∈ A.mask r, s e = w e) :
    acceptedThrough (prefixReplay A K) r s w π t =
      hiddenAcceptedThrough A r w π t := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.SecretaryReplay.prefixSet, OAI.MatroidProphet.acceptedThrough, OAI.MatroidProphet.SecretaryReplay.prefixReplay, OAI.MatroidProphet.hiddenAcceptedThrough
theorem OAI.MatroidProphet.SecretaryReplay.prefix_rejected line 95
Source documentation
The replay accepts nothing during the observation period.
```
theorem prefix_rejected {n bits : ℕ} (A : HiddenRule n bits) (K : ℕ)
    (r : Seed bits) (s v : Weights n) (π : ArrivalOrder n) {t : ℕ} (ht : t ≤ K) :
    acceptedThrough (prefixReplay A K) r s v π t = ∅ := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.acceptedThrough, OAI.MatroidProphet.SecretaryReplay.prefixReplay
theorem OAI.MatroidProphet.SecretaryReplay.fixedVector_reward line 107
Source documentation
All actual accepted weights equal their hidden-run weights.
```
theorem fixedVector_reward {n bits : ℕ} (A : HiddenRule n bits) (K : ℕ)
    (r : Seed bits) (s w : Weights n) (π : ArrivalOrder n)
    (hprefix : prefixSet π K ⊆ A.mask r)
    (hobs : ∀ e ∈ A.mask r, s e = w e) :
    reward (prefixReplay A K) r s w π = hiddenReward A r w π := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.SecretaryReplay.prefixSet, OAI.MatroidProphet.reward, OAI.MatroidProphet.SecretaryReplay.prefixReplay, OAI.MatroidProphet.hiddenReward
theorem OAI.MatroidProphet.SecretaryReplay.worstReward_le_replay line 117
Source documentation
Pointwise domination holds even when the order depends on extra visible secretary randomness beyond the reconstructed source seed.
```
theorem worstReward_le_replay {n bits : ℕ} (A : HiddenRule n bits) (K : ℕ)
    (r : Seed bits) (s w : Weights n) (π : ArrivalOrder n)
    (hprefix : prefixSet π K ⊆ A.mask r)
    (hobs : ∀ e ∈ A.mask r, s e = w e) :
    hiddenWorstReward A w r ≤ reward (prefixReplay A K) r s w π := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.SecretaryReplay.prefixSet, OAI.MatroidProphet.hiddenWorstReward, OAI.MatroidProphet.reward, OAI.MatroidProphet.SecretaryReplay.prefixReplay

theorem OAI.MatroidProphet.SecretaryReplay.fixedVector_feasible line 126

Source documentation

Pointwise feasibility of the source rule transfers at every replay prefix.

theorem fixedVector_feasible {n bits : ℕ} (M : Matroid (Fin n))
    (A : HiddenRule n bits) (K : ℕ)
    (hA : ∀ (w : Weights n), (∀ e, 0 ≤ w e) →
      ∀ (r : Seed bits) (π : ArrivalOrder n) (t : ℕ),
        M.Indep (hiddenAcceptedThrough A r w π t : Set (Fin n)))
    (r : Seed bits) (s w : Weights n) (π : ArrivalOrder n) (t : ℕ)
    (hw : ∀ e, 0 ≤ w e)
    (hprefix : prefixSet π K ⊆ A.mask r)
    (hobs : ∀ e ∈ A.mask r, s e = w e) :
    M.Indep (acceptedThrough (prefixReplay A K) r s w π t : Set (Fin n)) := by
…

Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.Seed, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough, OAI.MatroidProphet.SecretaryReplay.prefixSet, OAI.MatroidProphet.acceptedThrough, OAI.MatroidProphet.SecretaryReplay.prefixReplay