ReplayRule.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The actual history-only secretary rule reconstructed from a complete initial seed

The decoder consumes only the initial seed and the label set of the already observed prefix. The observation vector is extracted from actual past arrivals. A total mask-consistency guard rejects on unsupported decoder outcomes, ensuring feasibility for every initial seed rather than merely almost surely.

def OAI.MatroidProphet.SecretaryReplay.reconstructedRule line 22
Source documentation
A concrete secretary rule from a hidden rule and a precommitted decoder. The seed type is finite, but its law is arbitrary and need not be uniform.
```
noncomputable def reconstructedRule {n bits : ℕ} {Q : Type*}
    [Fintype Q] [MeasurableSpace Q] [MeasurableSingletonClass Q]
    (A : HiddenRule n bits) (K : Q → Fin (n + 1))
    (decode : Q → Finset (Fin n) → Seed bits) : SecretaryRule n Q where
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.SecretaryRule
theorem OAI.MatroidProphet.SecretaryReplay.decoder_history line 51
Source documentation
Once the prefix is complete, the decoder sees its full label set; no suffix label changes the reconstructed seed.
```
theorem decoder_history {n bits : ℕ} {Q : Type*}
    (K : Q → Fin (n + 1)) (decode : Q → Finset (Fin n) → Seed bits)
    (q : Q) (w : Weights n) (π : ArrivalOrder n) (k : Fin n)
    (hk : (K q).val ≤ k.val) :
    decode q (prefixLabels (K q).val (history w π k)) =
      decode q (orderPrefix π (K q).val) := by
…
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.prefixLabels, OAI.MatroidProphet.history, OAI.MatroidProphet.orderPrefix

theorem OAI.MatroidProphet.SecretaryReplay.reconstructed_acceptedThrough line 61

Source documentation

On mask-consistent outcomes the actual no-sample secretary execution exactly replays the hidden rule at every prefix.

theorem reconstructed_acceptedThrough {n bits : ℕ} {Q : Type*}
    [Fintype Q] [MeasurableSpace Q] [MeasurableSingletonClass Q]
    (A : HiddenRule n bits) (K : Q → Fin (n + 1))
    (decode : Q → Finset (Fin n) → Seed bits)
    (q : Q) (w : Weights n) (π : ArrivalOrder n) (t : ℕ)
    (hmask : A.mask (decode q (orderPrefix π (K q).val)) = orderPrefix π (K q).val) :
    secretaryAcceptedThrough (reconstructedRule A K decode) q w π t =
      hiddenAcceptedThrough A (decode q (orderPrefix π (K q).val)) w π t := by
…

Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.orderPrefix, OAI.MatroidProphet.secretaryAcceptedThrough, OAI.MatroidProphet.SecretaryReplay.reconstructedRule, OAI.MatroidProphet.hiddenAcceptedThrough

theorem OAI.MatroidProphet.SecretaryReplay.reconstructed_acceptedThrough_of_mismatch line 90

Source documentation

On an unsupported decoder outcome the total construction accepts nothing.

theorem reconstructed_acceptedThrough_of_mismatch {n bits : ℕ} {Q : Type*}
    [Fintype Q] [MeasurableSpace Q] [MeasurableSingletonClass Q]
    (A : HiddenRule n bits) (K : Q → Fin (n + 1))
    (decode : Q → Finset (Fin n) → Seed bits)
    (q : Q) (w : Weights n) (π : ArrivalOrder n) (t : ℕ)
    (hmask : A.mask (decode q (orderPrefix π (K q).val)) ≠ orderPrefix π (K q).val) :
    secretaryAcceptedThrough (reconstructedRule A K decode) q w π t = ∅ := by
…

theorem OAI.MatroidProphet.SecretaryReplay.reconstructed_feasible line 108

Source documentation

Feasibility is pointwise for every complete initial seed, including null outcomes of the conditional reconstruction kernels.

theorem reconstructed_feasible {n bits : ℕ} {Q : Type*}
    [Fintype Q] [MeasurableSpace Q] [MeasurableSingletonClass Q]
    (M : Matroid (Fin n)) (A : HiddenRule n bits)
    (K : Q → Fin (n + 1)) (decode : Q → Finset (Fin n) → Seed 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))) :
    SecretaryFeasible M (reconstructedRule A K decode) := by
…

Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough, OAI.MatroidProphet.SecretaryFeasible, OAI.MatroidProphet.SecretaryReplay.reconstructedRule

theorem OAI.MatroidProphet.SecretaryReplay.reconstructed_reward line 124

Source documentation

Exact replay includes reward, with the actual fixed vector on every accept.

theorem reconstructed_reward {n bits : ℕ} {Q : Type*}
    [Fintype Q] [MeasurableSpace Q] [MeasurableSingletonClass Q]
    (A : HiddenRule n bits) (K : Q → Fin (n + 1))
    (decode : Q → Finset (Fin n) → Seed bits)
    (q : Q) (w : Weights n) (π : ArrivalOrder n)
    (hmask : A.mask (decode q (orderPrefix π (K q).val)) = orderPrefix π (K q).val) :
    secretaryReward (reconstructedRule A K decode) q w π =
      hiddenReward A (decode q (orderPrefix π (K q).val)) w π := by
…

Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.orderPrefix, OAI.MatroidProphet.secretaryReward, OAI.MatroidProphet.SecretaryReplay.reconstructedRule, OAI.MatroidProphet.hiddenReward

theorem OAI.MatroidProphet.SecretaryReplay.worstReward_le_reconstructed line 136

Source documentation

The pointwise comparison permits arbitrary full-seed-aware suffix orders.

theorem worstReward_le_reconstructed {n bits : ℕ} {Q : Type*}
    [Fintype Q] [MeasurableSpace Q] [MeasurableSingletonClass Q]
    (A : HiddenRule n bits) (K : Q → Fin (n + 1))
    (decode : Q → Finset (Fin n) → Seed bits)
    (q : Q) (w : Weights n) (π : ArrivalOrder n)
    (hmask : A.mask (decode q (orderPrefix π (K q).val)) = orderPrefix π (K q).val) :
    hiddenWorstReward A w (decode q (orderPrefix π (K q).val)) ≤
      secretaryReward (reconstructedRule A K decode) q w π := by
…

Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.orderPrefix, OAI.MatroidProphet.hiddenWorstReward, OAI.MatroidProphet.secretaryReward, OAI.MatroidProphet.SecretaryReplay.reconstructedRule