Reviving the `leanprover-community/GameTheory` satellite repo idea (from #13248)

Following up on the discussion in #13248, and the same scope question that came up again on #39393.

Back in 2024, @urkud proposed on #13248: "I suggest that we create a new repository instead of pushing it to Mathlib right away. I can create leanprover-community/GameTheory this weekend, then push some basic theory there." @YaelDillies agreed the material isn't "abstract" enough for core Mathlib and needs room for experimentation. That repo doesn't seem to have been created, and #13248 has been sitting awaiting-author/merge-conflict since.

In the meantime @hcWang942 / Ma Jiajun's group kept building at math-xmum/gametheory:

• Zerosum.lean — a complete, 0-sorry, ~830-line proof of von Neumann's minimax theorem via Loomis's theorem
• Myerson.lean, Auction.lean, OptimalAuctionDesign.lean — mechanism design, mostly closed out
• Matching.lean — stable matching
• Nash1.lean / Sperner.lean — Nash equilibrium existence via Sperner's lemma toward Brouwer, still open (the fixed-point step is the hard part and isn't closed yet)

I've been independently working through Lean formalizations in adjacent areas: cooperative game theory (Shapley value, the Bondareva-Shapley core), evolutionary stable strategies, the folk theorem for repeated games, the Gibbard-Satterthwaite and Myerson-Satterthwaite impossibility theorems, Sion's minimax theorem (an independent route from Loomis's), Fenchel duality. I'd rather contribute that into a shared home than let it sit privately. I haven't cross-checked all of it against what's already in math-xmum/gametheory, so there's likely some overlap to sort out (e.g. matching/stable-matching), not a clean non-overlapping addition.

Given all this now genuinely exists across two groups and two years, would it make sense to actually revive the satellite-repo idea?

cc @urkud @YaelDillies @vihdzp who weighed in on scope before.

Read issues #13248 and #39393 first to understand the prior scope discussion. Compare the existing work in math-xmum/gametheory with the proposed formalizations, especially overlapping matching material; done means reaching a decision on whether to create and coordinate a shared satellite repository.