# One-sample matroid prophet inequalities against an almighty adversary

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [One Sample Suffices for Matroid Prophet Inequalities against an Almighty Adversary](../../preprints/One-Sample-Suffices-for-Matroid-Prophet-Inequalities-against-an-Almighty-Adversary-September-23-2026/final.pdf)

## Scope

The formalization proves a one-sample matroid prophet inequality with expected reward at least $2^{-310}$ times the expected offline optimum. Each element has one independent sample paired with an identically distributed nonnegative online value, and all coordinates are independent. The rule and finite seed law depend only on the labeled matroid; choices are irrevocable and feasible after every prefix. The arrival order may depend measurably on all samples, values, and the seed, and only the offline optimum must be integrable.

A supporting hidden-vector selection result for fixed nonnegative matroid weights gives expected worst-order reward at least $2^{-293}$ times the optimum, again with a finite seed law and prefix feasibility.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| One-sample matroid prophet inequality against an almighty adversary | [MatroidProphet.lean](../ComparatorChallenges/MatroidProphet.lean) |
| Hidden-vector matroid selection with worst-order guarantee | [MatroidSecretary.lean](../ComparatorChallenges/MatroidSecretary.lean) |