Proposition 27 — is a base of
ProvedMatroidOptGame.proposition_27approximation-algorithmscombinatorial-gamesmatroidsp2o-gran-per-chapterp2o-plan-paperp2o-v1
Let be a base of a matroid and let . Then is a base of the contraction .
The proof of Lemma 5 uses it to see that the invariant "two disjoint minimum-weight bases" survives a round of play.
Formalization Note Contraction is Mathlib's Matroid.contract by the singleton . The statement is for an arbitrary Mathlib matroid.
Differences from the source: none.
Preamble
import Mathlib
Formal statement
namespace MatroidOptGame
/-- **Proposition 27.** Let `B` be a base of `M` and `e ∈ B`. Then `B ∖ {e}` is a base of `M / e`.
Source: Jahn–Koolyk–Ostrovsky–Rabani–Schulman, *Approximation and Hardness in Optimization Games*,
STOC 2027 submission (manuscript sha256 7ad38b1a…dee74), Appendix A, Proposition 27, p.21. The `/` here is contraction (Appendix A,
p.19).
**Formalization Note.** Mathlib's contraction `M.contract {e}` (`M ／ {e}`); no finiteness or ground-set assumption
is needed. -/
theorem proposition_27 {α : Type*} (M : Matroid α) (B : Set α) (e : α) (hB : M.IsBase B)
(he : e ∈ B) : (M.contract {e}).IsBase (B \ {e}) := by sorry
end MatroidOptGame
Source
Jahn–Koolyk–Ostrovsky–Rabani–Schulman, Approximation and Hardness in Optimization Games, STOC 2027 submission (manuscript sha256 7ad38b1a…dee74), Appendix A, Proposition 27, p.21
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.