ReplayFacts.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Deterministic replay for the secretary transport

This optional supplement uses a distinct namespace so it can coexist with the canonical SecretaryReplay implementation without duplicate declaration names.

These lemmas concern the replay step in the proof of cor:secretary in the pinned sections/secretary.tex. They do not assert or assume the random-prefix law. The latter is a separate probability obligation. A reconstructed seed may be any function of the secretary seed and observed prefix: all the results below hold pointwise for every seed and every completed arrival permutation.

lemma OAI.MatroidProphet.SecretaryReplaySupplement.glue_eq_of_agree line 25
Source documentation
Agreement on the sacrificed labels is the exact information needed to replay an actual fixed vector. Values supplied outside that mask are irrelevant.
```
lemma glue_eq_of_agree {n : ℕ} (mask : Finset (Fin n)) (s w : Weights n)
    (hs : ∀ e ∈ mask, s e = w e) : glue mask s w = w := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.glue
lemma OAI.MatroidProphet.SecretaryReplaySupplement.observed_agrees line 33
lemma OAI.MatroidProphet.SecretaryReplaySupplement.history_replay line 41
Source documentation
The actual current and past label--weight pairs, including rejected prefix arrivals, are passed to the source core unchanged.
```
lemma history_replay {n bits : ℕ} (A : HiddenRule n bits) (r : Seed bits)
    (s w : Weights n) (hs : ∀ e ∈ A.mask r, s e = w e)
    (π : ArrivalOrder n) (k : Fin n) :
    simulationHistory A r s (history w π k) = history w π k := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.simulationHistory, OAI.MatroidProphet.history
theorem OAI.MatroidProphet.SecretaryReplaySupplement.acceptedThrough_replay line 48
Source documentation
Exact accepted-set identity at every time, not just equality of total reward.
```
theorem acceptedThrough_replay {n bits : ℕ} (A : HiddenRule n bits) (r : Seed bits)
    (s w : Weights n) (hs : ∀ e ∈ A.mask r, s e = w e)
    (π : ArrivalOrder n) (t : ℕ) :
    acceptedThrough (sampleSimulation A) 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.acceptedThrough, OAI.MatroidProphet.sampleSimulation, OAI.MatroidProphet.hiddenAcceptedThrough
theorem OAI.MatroidProphet.SecretaryReplaySupplement.reward_replay line 56
Source documentation
Replay never replaces a realized payoff by a sampled or auxiliary value.
```
theorem reward_replay {n bits : ℕ} (A : HiddenRule n bits) (r : Seed bits)
    (s w : Weights n) (hs : ∀ e ∈ A.mask r, s e = w e)
    (π : ArrivalOrder n) :
    reward (sampleSimulation A) r s w π = hiddenReward A r w π := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.reward, OAI.MatroidProphet.sampleSimulation, OAI.MatroidProphet.hiddenReward
theorem OAI.MatroidProphet.SecretaryReplaySupplement.observed_replay line 63
Source documentation
Only the revealed vector is needed for the initial observation.
```
theorem observed_replay {n bits : ℕ} (A : HiddenRule n bits) (r : Seed bits)
    (w : Weights n) (π : ArrivalOrder n) (t : ℕ) :
    acceptedThrough (sampleSimulation A) r (observed A r w) w π t =
      hiddenAcceptedThrough A r w π t :=
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.acceptedThrough, OAI.MatroidProphet.sampleSimulation, OAI.MatroidProphet.observed, OAI.MatroidProphet.hiddenAcceptedThrough
theorem OAI.MatroidProphet.SecretaryReplaySupplement.prefix_rejected line 71
Source documentation
If the mask is exactly the observed prefix set, no prefix label is accepted. The bound includes both zero-length and full-length prefixes.
```
theorem prefix_rejected {n bits : ℕ} (A : HiddenRule n bits) (r : Seed bits)
    (s w : Weights n) (π : ArrivalOrder n) (K : ℕ)
    (hmask : ∀ e, e ∈ A.mask r ↔ (π.symm e).val < K) :
    acceptedThrough (sampleSimulation A) r s w π K = ∅ := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.acceptedThrough, OAI.MatroidProphet.sampleSimulation
theorem OAI.MatroidProphet.SecretaryReplaySupplement.accepted_after_prefix line 83
Source documentation
The prefix is still excluded at all later times.
```
theorem accepted_after_prefix {n bits : ℕ} (A : HiddenRule n bits) (r : Seed bits)
    (s w : Weights n) (π : ArrivalOrder n) (K t : ℕ)
    (hmask : ∀ e, e ∈ A.mask r ↔ (π.symm e).val < K)
    {e : Fin n} (he : e ∈ acceptedThrough (sampleSimulation A) r s w π t) :
    K ≤ (π.symm e).val := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.acceptedThrough, OAI.MatroidProphet.sampleSimulation
theorem OAI.MatroidProphet.SecretaryReplaySupplement.worstReward_le_replay line 94
Source documentation
An arbitrary suffix order, even one knowing all unused seed coordinates, cannot defeat the pointwise minimum over completed permutations.
```
theorem worstReward_le_replay {n bits : ℕ} (A : HiddenRule n bits) (r : Seed bits)
    (s w : Weights n) (hs : ∀ e ∈ A.mask r, s e = w e)
    (π : ArrivalOrder n) :
    hiddenWorstReward A w r ≤ reward (sampleSimulation A) r s w π := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenWorstReward, OAI.MatroidProphet.reward, OAI.MatroidProphet.sampleSimulation

theorem OAI.MatroidProphet.SecretaryReplaySupplement.feasible_replay line 103

Source documentation

Every-prefix matroid feasibility transfers without a condition on the suffix adversary or on weights assigned outside the observation mask.

theorem feasible_replay {n bits : ℕ} (M : Matroid (Fin n)) (A : HiddenRule n bits)
    (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) (hw : ∀ e, 0 ≤ w e)
    (hs : ∀ e ∈ A.mask r, s e = w e) (π : ArrivalOrder n) (t : ℕ) :
    M.Indep (acceptedThrough (sampleSimulation A) 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.acceptedThrough, OAI.MatroidProphet.sampleSimulation