SimulationInformation.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Information restrictions of the one-sample simulation

These pointwise statements make explicit the information restrictions used in sections/setup.tex, Lemma lem:simulation: unused samples and online values of sacrificed labels cannot affect the execution. The final two replay identities also support the prefix/suffix construction in sections/secretary.tex. No independence, positivity, or feasibility assumptions are needed for these deterministic identities.

lemma OAI.MatroidProphet.simulationObserved_eq_of_eq_on_mask line 18
lemma OAI.MatroidProphet.simulationHistory_eq_of_eq_on_mask line 28
theorem OAI.MatroidProphet.sampleSimulation_decide_eq_of_eq_on_mask line 39
Source documentation
The simulator's current decision ignores every sample outside its mask.
```
theorem sampleSimulation_decide_eq_of_eq_on_mask {n bits : ℕ}
    (A : HiddenRule n bits) (r : Seed bits) (s s' : Weights n)
    (k : Fin n) (h : History n k)
    (hs : ∀ e ∈ A.mask r, s e = s' e) :
    (sampleSimulation A).decide k r s h =
      (sampleSimulation A).decide k r s' h := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.History, OAI.MatroidProphet.sampleSimulation
lemma OAI.MatroidProphet.glue_eq_of_eq_on_regions line 50

theorem OAI.MatroidProphet.sampleSimulation_acceptedThrough_noninterference line 62

Source documentation

Neither unused samples nor sacrificed online values change any accepted prefix.

theorem sampleSimulation_acceptedThrough_noninterference {n bits : ℕ}
    (A : HiddenRule n bits) (r : Seed bits) (s s' v v' : Weights n)
    (π : ArrivalOrder n) (t : ℕ)
    (hs : ∀ e ∈ A.mask r, s e = s' e)
    (hv : ∀ e ∉ A.mask r, v e = v' e) :
    acceptedThrough (sampleSimulation A) r s v π t =
      acceptedThrough (sampleSimulation A) r s' v' π t := by
…

Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.acceptedThrough, OAI.MatroidProphet.sampleSimulation

theorem OAI.MatroidProphet.sampleSimulation_reward_noninterference line 73
Source documentation
The same information invariance holds for the reward in actual online values.
```
theorem sampleSimulation_reward_noninterference {n bits : ℕ}
    (A : HiddenRule n bits) (r : Seed bits) (s s' v v' : Weights n)
    (π : ArrivalOrder n)
    (hs : ∀ e ∈ A.mask r, s e = s' e)
    (hv : ∀ e ∉ A.mask r, v e = v' e) :
    reward (sampleSimulation A) r s v π =
      reward (sampleSimulation A) r s' v' π := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.reward, OAI.MatroidProphet.sampleSimulation
theorem OAI.MatroidProphet.sampleSimulation_rejects_mask line 84
Source documentation
A sacrificed label is rejected at every prefix, irrespective of its value.
```
theorem sampleSimulation_rejects_mask {n bits : ℕ} (A : HiddenRule n bits)
    (r : Seed bits) (s v : Weights n) (π : ArrivalOrder n) (t : ℕ)
    (e : Fin n) (he : e ∈ A.mask r) :
    e ∉ acceptedThrough (sampleSimulation A) r s v π t := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.acceptedThrough, OAI.MatroidProphet.sampleSimulation
lemma OAI.MatroidProphet.glue_observed_left line 91
theorem OAI.MatroidProphet.sampleSimulation_replay_acceptedThrough line 100
Source documentation
Replaying the full arrived history after supplying only the observed mask agrees exactly with the hidden rule, at every prefix including zero.
```
theorem sampleSimulation_replay_acceptedThrough {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 := by
…
```
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.sampleSimulation_replay_reward line 108
Source documentation
The replay identity preserves the actual reward without a numerical loss.
```
theorem sampleSimulation_replay_reward {n bits : ℕ}
    (A : HiddenRule n bits) (r : Seed bits) (w : Weights n)
    (π : ArrivalOrder n) :
    reward (sampleSimulation A) r (observed A r w) 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.observed, OAI.MatroidProphet.hiddenReward