"Formally Verified Pok\u00e9mon TCG Metagame Analysis: Tournament Data, Matchup Matrices, and Lean 4 Proof Artifact"

"This dataset contains pairwise matchup win rates, win-loss-tie records, and metagame share data for 14 archetypes in competitive Pok\u00e9mon Trading Card Game tournaments (January\u2013February 2026), collected from Trainer Hill across events with 50 or more players during the Stellar Crown\u2013Prismatic Evolutions format. The full 14\u00d714 matchup matrix encompasses thousands of recorded matches with complete win-loss-tie counts per ordered pair. Accompanying computed results include asymmetric and symmetric Nash equilibrium strategies, a 10,000-iteration bootstrap stability analysis with Wilson 95% confidence intervals, single-step replicator dynamics predictions with empirical validation against observed metagame trends, and a trust boundary audit of all native_decide proof closures. All game-theoretic claims derived from this data are formally verified in a Lean 4 artifact spanning approximately 30,000 lines and 2,500 theorems with no sorry, admit, or custom axioms. The dataset supports reproducible research in formal verification, metagame analysis, and computational game theory. "