InformationRestriction.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Explicit information restrictions for hidden-vector rules

These lemmas formalize the no-future-information and irrevocability clauses of sections/algorithm.tex, Lemma lem:feasibility. They use only the concrete history and acceptance definitions; no correctness hypothesis for an algorithm is introduced.

lemma OAI.MatroidProphet.observed_eq_of_eq_on_mask line 18
lemma OAI.MatroidProphet.history_eq_of_agree_before line 28
theorem OAI.MatroidProphet.acceptedThrough_eq_of_agree_before line 38
Source documentation
Equal available label/value pairs give the same accepted set through a prefix. The two complete arrival orders and all later values may be different.
```
theorem acceptedThrough_eq_of_agree_before {n bits : ℕ} (A : OnlineRule n bits)
    (r : Seed bits) (s v v' : Weights n) (π π' : ArrivalOrder n) (t : ℕ)
    (h : ∀ j : Fin n, j.val < t → (π j, v (π j)) = (π' j, v' (π' j))) :
    acceptedThrough A r s v π t = acceptedThrough A r s v' π' t := by
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.acceptedThrough
theorem OAI.MatroidProphet.hiddenAcceptedThrough_eq_of_same_information line 65
Source documentation
A hidden-vector execution depends only on its revealed coordinates and the actual arrival history, never on the unobserved future values or future order.
```
theorem hiddenAcceptedThrough_eq_of_same_information {n bits : ℕ}
    (A : HiddenRule n bits) (r : Seed bits) (w w' : Weights n)
    (π π' : ArrivalOrder n) (t : ℕ)
    (hmask : ∀ e ∈ A.mask r, w e = w' e)
    (hhist : ∀ j : Fin n, j.val < t →
      (π j, w (π j)) = (π' j, w' (π' j))) :
    hiddenAcceptedThrough A r w π t = hiddenAcceptedThrough A r w' π' t := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough
theorem OAI.MatroidProphet.hiddenAcceptedThrough_monotone line 77
Source documentation
Hidden-vector acceptances cannot be revoked.
```
theorem hiddenAcceptedThrough_monotone {n bits : ℕ} (A : HiddenRule n bits)
    (r : Seed bits) (w : Weights n) (π : ArrivalOrder n) :
    Monotone (hiddenAcceptedThrough A r w π) := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough
theorem OAI.MatroidProphet.hiddenAcceptedThrough_disjoint_mask line 86
Source documentation
Sacrifice is literal rejection, not merely exclusion from the reward sum.
```
theorem hiddenAcceptedThrough_disjoint_mask {n bits : ℕ} (A : HiddenRule n bits)
    (r : Seed bits) (w : Weights n) (π : ArrivalOrder n) (t : ℕ) :
    Disjoint (hiddenAcceptedThrough A r w π t) (A.mask r) := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough
theorem OAI.MatroidProphet.hiddenAcceptedThrough_arrived line 92
Source documentation
Every accepted hidden-vector label has actually arrived.
```
theorem hiddenAcceptedThrough_arrived {n bits : ℕ} (A : HiddenRule n bits)
    (r : Seed bits) (w : Weights n) (π : ArrivalOrder n) (t : ℕ)
    (e : Fin n) (he : e ∈ hiddenAcceptedThrough A r w π t) :
    (π.symm e).val < t :=
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough
lemma OAI.MatroidProphet.measurable_observed_seed line 101
Source documentation
The observation operation is jointly measurable in the complete initial seed and the hidden vector, despite an arbitrary seed-dependent mask.
```
lemma measurable_observed_seed {n bits : ℕ} (A : HiddenRule n bits) :
    Measurable (fun x : Seed bits × Weights n => observed A x.1 x.2) := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.observed
lemma OAI.MatroidProphet.measurable_hidden_core_decide line 115
Source documentation
With observations substituted, the actual core decision remains measurable.
```
lemma measurable_hidden_core_decide {n bits : ℕ} (A : HiddenRule n bits)
    (k : Fin n) :
    Measurable (fun x : Seed bits × (Weights n × History n k) =>
      A.core.decide k x.1 (observed A x.1 x.2.1) x.2.2) := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.History, OAI.MatroidProphet.observed