Final.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The full-seed order-oblivious secretary consequence

The concrete initial seed law is fixed before the weight vector. The complete conditional table is drawn initially and the decoder uses only prefix labels. The actual rule's guarded replay is feasible at every seed, while the exact source-law coupling supplies the expected-minimum guarantee against every measurable full-information suffix policy.

theorem OAI.MatroidProphet.secretary line 19
Source documentation
cor:secretary, with no construction-law or model-validity assumption.
```
theorem secretary.{u} : SecretaryChallenge.{u} := by
…
```