OAI/Probability/MatroidSecretary/Secretary/Model.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Online information model for the full-seed secretary consequence
The rule precommits its prefix length using only its complete initial seed. Its current decision sees exactly that seed and the currently available ordered label–weight history, with no sample vector and no future suffix permutation. Observation-prefix arrivals are unconditionally rejected by the execution model.
This file declares nothing itself. It gathers the import below, so a file that imports it gets all of them.