OAI/Probability/MatroidSecretary/Labels/RelabelingCompatibility.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact agreement of two independently developed finite-label interfaces. The bundled-rule presentation and the earlier canonical transport evaluate the same concrete decisions, accepted prefixes, rewards, and offline benchmark.

  1. theorem OAI.MatroidProphet.LabeledTransport.optimum_eq_canonical line 16
  2. theorem OAI.MatroidProphet.LabeledTransport.decode_decide_eq_canonical line 19
  3. theorem OAI.MatroidProphet.LabeledTransport.decode_accepted_eq_canonical line 24
  4. theorem OAI.MatroidProphet.LabeledTransport.decode_reward_eq_canonical line 30