# Capability matrix

This matrix describes recognizable workflows supported by the current public
library. It is successor-native: evidence points to compiled modules and stable
discriminating examples, not to declaration ancestry.

Verdicts mean:

- **supported**: the public API and a representative semantic consumer build;
- **partial**: a useful stable surface exists, with a named mathematical limit;
- **opt-in**: supported outside the light default root; and
- **frontier**: intentionally absent from the stable library.

## Static and analytic game theory

| Workflow | Public evidence | Verdict | Limit or next seam |
|---|---|---|---|
| Import the coordinated analytic surface | [`GameTheory/Analysis.lean`](../GameTheory/Analysis.lean) | opt-in | Semantic roots do not import the analytic aggregator. |
| Define strategic forms, profiles, preferences, deviations, and Nash-like concepts | [`GameTheory/Core.lean`](../GameTheory/Core.lean) | supported | Keep one canonical equilibrium predicate and explicit deviation schemes. |
| Transport equilibrium across outcome, player, and strategy relabeling | [`GameTheory/Core/Transform.lean`](../GameTheory/Core/Transform.lean), [`GameTheory/Tests/Transform.lean`](../GameTheory/Tests/Transform.lean) | supported | Nash/CCE/CE squares and both mixed-play commutation laws are explicit; no generic morphism hierarchy is implied. |
| Prove finite-law event and Markov bounds | [`GameTheory/Math/Probability/Bounds.lean`](../GameTheory/Math/Probability/Bounds.lean), [`GameTheory/Tests/ProbabilityBounds.lean`](../GameTheory/Tests/ProbabilityBounds.lean) | supported | Nonnegativity is needed only on finite support; general measurable concentration belongs in a separate analytic layer. |
| Pass finite-law pointwise limits through expectations and independent products | [`GameTheory/Math/Probability/Convergence.lean`](../GameTheory/Math/Probability/Convergence.lean), [`GameTheory/Analysis/ExpectedUtility.lean`](../GameTheory/Analysis/ExpectedUtility.lean) | supported | The reusable theorem is for finite carriers; measurable weak convergence is a separate layer. |
| Compute finite pure Nash over rational tables | [`GameTheory/Finite/Algorithm.lean`](../GameTheory/Finite/Algorithm.lean), [`GameTheory/Finite/Correctness.lean`](../GameTheory/Finite/Correctness.lean), [`GameTheory/Examples/Classic.lean`](../GameTheory/Examples/Classic.lean) | supported | Execution stays separate from real-valued proof semantics. |
| Obtain finite mixed Nash and correlated-equilibrium existence | [`GameTheory/Analysis/Nash.lean`](../GameTheory/Analysis/Nash.lean), [`GameTheory/Analysis/Correlated.lean`](../GameTheory/Analysis/Correlated.lean) | opt-in | No general equilibrium solver is implied. |
| Certify correlated equilibrium from local recommendation obedience | [`GameTheory/Core/CorrelatedDominance.lean`](../GameTheory/Core/CorrelatedDominance.lean), [`GameTheory/Tests/CorrelatedDominance.lean`](../GameTheory/Tests/CorrelatedDominance.lean) | supported | Only recommendations with positive mass require checks; no finite strategy-carrier assumption is stored. |
| Certify and reconstruct Bayes-correlated equilibrium | [`GameTheory/Core/BayesCorrelated.lean`](../GameTheory/Core/BayesCorrelated.lean), [`GameTheory/Tests/BayesCorrelated.lean`](../GameTheory/Tests/BayesCorrelated.lean), [`GameTheory/Tests/Revelation.lean`](../GameTheory/Tests/Revelation.lean) | supported | Positive-cell interim obedience is equivalent to BCE; every BCE is reconstructed as the exact outcome law of a Bayes–Nash action-signal structure. |
| Prove no-regret to approximate CCE and multiplicative-weights consequences | [`GameTheory/Core/Learning.lean`](../GameTheory/Core/Learning.lean), [`GameTheory/Math/OnlineLearning.lean`](../GameTheory/Math/OnlineLearning.lean), [`GameTheory/Analysis/Learning.lean`](../GameTheory/Analysis/Learning.lean) | supported | Includes fixed-rate, arbitrary-tolerance, and tuned `2√(LT)` bounds; weighted-potential extensions remain separate. |
| Convert two-player zero-sum external-regret bounds into empirical saddle gaps and approximate mixed Nash | [`GameTheory/Analysis/ZeroSumLearning.lean`](../GameTheory/Analysis/ZeroSumLearning.lean), [`GameTheory/Analysis/ZeroSumLearningTest.lean`](../GameTheory/Analysis/ZeroSumLearningTest.lean) | opt-in | The trace law may be correlated and both marginals are derived; dynamic bounds remain the caller's input. |
| Run two Protocol regret learners on one zero-sum trace and obtain empirical approximate Nash | [`GameTheory/Analysis/Protocol/CounterfactualZeroSumLearningTest.lean`](../GameTheory/Analysis/Protocol/CounterfactualZeroSumLearningTest.lean) | opt-in | The compiled consumer has two moving one-site learners and vanishing canonical Nash tolerance. General multi-site schedule synthesis is not claimed. |
| Learn over multiple Bayesian information sites and obtain empirical approximate Nash over complete contingent plans | [`GameTheory/Analysis/Protocol/BayesianZeroSumLearningTest.lean`](../GameTheory/Analysis/Protocol/BayesianZeroSumLearningTest.lean) | opt-in | Four actual shared-profile local learners cover two positive-mass types per player; reusable scheduler synthesis, arbitrary behavioral replacements, and unequal-depth fibers remain separate. |
| Construct and analyze fictitious play | [`GameTheory/Core/FictitiousPlay.lean`](../GameTheory/Core/FictitiousPlay.lean), [`GameTheory/Tests/FictitiousPlay.lean`](../GameTheory/Tests/FictitiousPlay.lean), [`GameTheory/Analysis/FictitiousPlayTest.lean`](../GameTheory/Analysis/FictitiousPlayTest.lean) | supported | The analytic consumer proves a forever-changing path converges to mixed Nash. |
| Use Blackwell approachability and regret matching | [`GameTheory/Math/Approachability.lean`](../GameTheory/Math/Approachability.lean), [`GameTheory/Tests/Approachability.lean`](../GameTheory/Tests/Approachability.lean) | opt-in | Response selection is proof-facing and stationary in the running average. |
| Reason about dominance, correlated and independent rationalizability, pure elimination, response dynamics, and weak acyclicity | [`GameTheory/Core/Response.lean`](../GameTheory/Core/Response.lean), [`GameTheory/Core/Rationalizability.lean`](../GameTheory/Core/Rationalizability.lean), [`GameTheory/Tests/Rationalizability.lean`](../GameTheory/Tests/Rationalizability.lean) | supported | Independent beliefs use the canonical mixed-product law, imply correlated rationalizability, and are strictly separated from its converse in a three-player fixture; pure-elimination survival retains its distinct name. |
| Use exact, ordinal, and mixed potential games | [`GameTheory/Core/Potential.lean`](../GameTheory/Core/Potential.lean), [`GameTheory/Core/MixedPotential.lean`](../GameTheory/Core/MixedPotential.lean), [`GameTheory/Tests/Potential.lean`](../GameTheory/Tests/Potential.lean) | supported | Weighted potential is not folded into the exact predicate. |
| Analyze zero-sum matrix security, maximin--minimax equality, and selected values | [`GameTheory/Core/MatrixGame.lean`](../GameTheory/Core/MatrixGame.lean), [`GameTheory/Analysis/Minimax.lean`](../GameTheory/Analysis/Minimax.lean) | supported | General measurable games are outside scope. |
| Use finite-outcome expected-utility representation and affine uniqueness | [`GameTheory/Core/VNM.lean`](../GameTheory/Core/VNM.lean), [`GameTheory/Tests/VNM.lean`](../GameTheory/Tests/VNM.lean) | supported | Infinite-outcome representation needs a separate analytic layer. |
| Apply Arrow, Gibbard–Satterthwaite, and May | [`GameTheory/Core/Arrow.lean`](../GameTheory/Core/Arrow.lean), [`GameTheory/Core/GibbardSatterthwaite.lean`](../GameTheory/Core/GibbardSatterthwaite.lean), [`GameTheory/Core/May.lean`](../GameTheory/Core/May.lean) | supported | Sen and median-voter extensions remain open. |
| State coalitional games, Shapley values, balancedness, and voting power | [`GameTheory/Cooperative.lean`](../GameTheory/Cooperative.lean), [`GameTheory/Tests/Banzhaf.lean`](../GameTheory/Tests/Banzhaf.lean), [`GameTheory/Tests/Shapley.lean`](../GameTheory/Tests/Shapley.lean) | opt-in | The hard balancedness converse and convex-game core theorem remain open. |
| Use static ESS/NSS and the symmetric Nash bridge | [`GameTheory/Evolutionary.lean`](../GameTheory/Evolutionary.lean), [`GameTheory/Tests/Evolutionary.lean`](../GameTheory/Tests/Evolutionary.lean) | supported | No population dynamics claim is made. |
| Reason about knowledge, conditioned posteriors, common knowledge, and agreement | [`GameTheory/Epistemic.lean`](../GameTheory/Epistemic.lean), [`GameTheory/Tests/Agreement.lean`](../GameTheory/Tests/Agreement.lean) | supported | Finite-cell posteriors equal canonical conditioning on positive cells; a Protocol bridge still needs an explicit state-view premise. |
| Prove Rosenthal potential and affine price-of-anarchy bounds | [`GameTheory/Congestion.lean`](../GameTheory/Congestion.lean), [`GameTheory/Tests/Congestion.lean`](../GameTheory/Tests/Congestion.lean) | opt-in | Congestion stays layered over canonical potential and welfare theory. |

## Sequential, repeated, and stochastic theory

| Workflow | Public evidence | Verdict | Limit or next seam |
|---|---|---|---|
| Model execution, chance, histories, information-local policies, and behavioral laws | [`GameTheory/Protocol.lean`](../GameTheory/Protocol.lean) | supported | No universal game hub or duplicate runner. |
| Extract strategic forms and transfer pure/mixed Nash | [`GameTheory/Languages/EFG/Strategic.lean`](../GameTheory/Languages/EFG/Strategic.lean) | supported | Extraction forgets sequential structure. |
| State textbook subgame perfection under imperfect information | [`GameTheory/Protocol/SubgamePerfect.lean`](../GameTheory/Protocol/SubgamePerfect.lean), [`GameTheory/Languages/EFG/SubgamePerfect.lean`](../GameTheory/Languages/EFG/SubgamePerfect.lean), [`GameTheory/Tests/SubgameRoots.lean`](../GameTheory/Tests/SubgameRoots.lean), [`GameTheory/Tests/SubgameOneShot.lean`](../GameTheory/Tests/SubgameOneShot.lean) | supported | Whole-policy deviations are essential: single-information-state tests do not characterize SPE even under perfect recall. Point-mass continuation evaluation hides support-dependent proof transport for deterministic EFGs. |
| Construct a pure SPE by backward induction | [`GameTheory/Protocol/Zermelo.lean`](../GameTheory/Protocol/Zermelo.lean), [`GameTheory/Tests/EFGZermelo.lean`](../GameTheory/Tests/EFGZermelo.lean), [`GameTheory/Tests/ZermeloMenus.lean`](../GameTheory/Tests/ZermeloMenus.lean) | supported | Requires well-founded single-mover play, separated decision histories, a total fallback plan, and finite choices only at genuine decision histories; unreachable choice carriers may be infinite. |
| Move between behavioral and mixed strategies under perfect recall | [`GameTheory/Protocol/Strategic.lean`](../GameTheory/Protocol/Strategic.lean), [`GameTheory/Protocol/PolicyMeasure.lean`](../GameTheory/Protocol/PolicyMeasure.lean), [`GameTheory/Languages/EFG/Kuhn.lean`](../GameTheory/Languages/EFG/Kuhn.lean), [`GameTheory/Stochastic/Kuhn.lean`](../GameTheory/Stochastic/Kuhn.lean), [`GameTheory/Experimental/PostArchitecture/KuhnFiniteSupport.lean`](../GameTheory/Experimental/PostArchitecture/KuhnFiniteSupport.lean), [`GameTheory/Experimental/PostArchitecture/StochasticKuhn.lean`](../GameTheory/Experimental/PostArchitecture/StochasticKuhn.lean), [`GameTheory/Experimental/PostArchitecture/StochasticInfiniteKuhn.lean`](../GameTheory/Experimental/PostArchitecture/StochasticInfiniteKuhn.lean), [`GameTheory/Experimental/PostArchitecture/StochasticReverseInfiniteKuhn.lean`](../GameTheory/Experimental/PostArchitecture/StochasticReverseInfiniteKuhn.lean), [`GameTheory/Experimental/PostArchitecture/StochasticHybridInfiniteKuhn.lean`](../GameTheory/Experimental/PostArchitecture/StochasticHybridInfiniteKuhn.lean), [`GameTheory/Tests/EFGKuhnNash.lean`](../GameTheory/Tests/EFGKuhnNash.lean) | supported | Bounded whole-profile laws require no ambient information-state finiteness; finite counterfactual covers add exact unilateral updated laws and Nash transfer. EXP-117/D57 supplies one horizon-independent regular forward product law. EXP-118/D58 reads arbitrary independent per-player policy measures through finite own-record conditioning. EXP-119/D59 supplies both hybrid deviation laws—arbitrary policy-law opponents with a behavioral focal deviation, and behavioral opponents with an arbitrary policy-law focal deviation—with exact all-prefix and discounted consequences. The unbounded `FinDist` convenience, correlated joint player laws, and infinite-path outcome semantics remain separate. |
| Use sequential equilibrium with finite behavioral assessments | [`GameTheory/Analysis/Protocol/EFG.lean`](../GameTheory/Analysis/Protocol/EFG.lean), [`GameTheory/Analysis/Protocol/EFGTest.lean`](../GameTheory/Analysis/Protocol/EFGTest.lean) | opt-in | Bayes consistency requires decision fibers to be history antichains; perfect recall is sufficient. |
| Use trembling-hand perfection | [`GameTheory/Analysis/TremblingHand.lean`](../GameTheory/Analysis/TremblingHand.lean), [`GameTheory/Analysis/TremblingHandTest.lean`](../GameTheory/Analysis/TremblingHandTest.lean) | opt-in | Alternative refinement predicates are not conflated. |
| Model deterministic repeated play, public-signal monitoring and rank, APS self-generation, triggers, PPE, and uniform equilibrium | [`GameTheory/Repeated.lean`](../GameTheory/Repeated.lean), [`GameTheory/Tests/MonitoringRank.lean`](../GameTheory/Tests/MonitoringRank.lean), [`GameTheory/Tests/MonitoringSelfGeneration.lean`](../GameTheory/Tests/MonitoringSelfGeneration.lean), [`GameTheory/Tests/MonitoringEquilibrium.lean`](../GameTheory/Tests/MonitoringEquilibrium.lean), [`GameTheory/Tests/RepeatedUniform.lean`](../GameTheory/Tests/RepeatedUniform.lean) | supported | Self-generation covers bounded pure-public payoff sets; public lotteries and a stable infinite realized-path law remain outside this surface. EXP-108/113 validate an experiment-only canonical finite-marginal path measure, a nonconstant stochastic-game consumer, and separate long-run payoff results. Cyclic subgame-perfect uniformity remains open. |
| Use finite stochastic games, chronological horizon laws, Kuhn, restarts, and uniform payoff certificates | [`GameTheory/Stochastic/PublicPolicy.lean`](../GameTheory/Stochastic/PublicPolicy.lean), [`GameTheory/Stochastic/History.lean`](../GameTheory/Stochastic/History.lean), [`GameTheory/Stochastic/Kuhn.lean`](../GameTheory/Stochastic/Kuhn.lean), [`GameTheory/Experimental/PostArchitecture/StochasticInfiniteKuhn.lean`](../GameTheory/Experimental/PostArchitecture/StochasticInfiniteKuhn.lean), [`GameTheory/Experimental/PostArchitecture/StochasticReverseInfiniteKuhn.lean`](../GameTheory/Experimental/PostArchitecture/StochasticReverseInfiniteKuhn.lean), [`GameTheory/Experimental/PostArchitecture/StochasticHybridInfiniteKuhn.lean`](../GameTheory/Experimental/PostArchitecture/StochasticHybridInfiniteKuhn.lean), [`GameTheory/Tests/StochasticContinuation.lean`](../GameTheory/Tests/StochasticContinuation.lean), [`GameTheory/Examples/StochasticUniform.lean`](../GameTheory/Examples/StochasticUniform.lean) | opt-in | Ordinary public policies compile losslessly to canonical Protocol behavior; bounded Kuhn needs finite players/actions but neither finite states nor finite public histories. On countable state spaces, one regular forward law realizes every prefix and discounted payoff; arbitrary supplied independent policy measures admit the reverse behavioral reading even without regularity, and both hybrid unilateral deviation quantifiers preserve all prefixes and bounded discounted payoff. No stable infinite-path outcome law, correlated joint-law representation, or general uniform existence is claimed. EXP-108/113 validate the separate experiment-only path measure; the cyclic all-phase consumer remains open. |
| Use discounted zero-sum and stationary general-sum stochastic values | [`GameTheory/Analysis/Stochastic.lean`](../GameTheory/Analysis/Stochastic.lean) | opt-in | General-sum theorem is a stationary Bellman certificate, not arbitrary history-dependent equilibrium. |

## Languages and mechanisms

| Workflow | Public evidence | Verdict | Limit or next seam |
|---|---|---|---|
| Write deterministic normal-form syntax and compile directly to the static core | [`GameTheory/Languages/NFG.lean`](../GameTheory/Languages/NFG.lean) | supported | No language-specific Nash predicate. |
| Model simultaneous stochastic observation, serialize FOSG to EFG, and analyze counterfactual deviations | [`GameTheory/Languages/Bridges/FOSGToEFG.lean`](../GameTheory/Languages/Bridges/FOSGToEFG.lean), [`GameTheory/Languages/Bridges/FOSGToEFGStrategic.lean`](../GameTheory/Languages/Bridges/FOSGToEFGStrategic.lean), [`GameTheory/Analysis/Protocol/CounterfactualReach.lean`](../GameTheory/Analysis/Protocol/CounterfactualReach.lean), [`GameTheory/Analysis/Protocol/CounterfactualRegret.lean`](../GameTheory/Analysis/Protocol/CounterfactualRegret.lean), [`GameTheory/Analysis/Protocol/CounterfactualRegretMatching.lean`](../GameTheory/Analysis/Protocol/CounterfactualRegretMatching.lean), [`GameTheory/Analysis/Protocol/CounterfactualDecomposition.lean`](../GameTheory/Analysis/Protocol/CounterfactualDecomposition.lean), [`GameTheory/Analysis/Protocol/CounterfactualRootRegret.lean`](../GameTheory/Analysis/Protocol/CounterfactualRootRegret.lean), [`GameTheory/Analysis/Protocol/CounterfactualRootRegretTest.lean`](../GameTheory/Analysis/Protocol/CounterfactualRootRegretTest.lean), [`GameTheory/Analysis/Protocol/CounterfactualZeroSumLearningTest.lean`](../GameTheory/Analysis/Protocol/CounterfactualZeroSumLearningTest.lean), [`GameTheory/Analysis/Protocol/BayesianZeroSumLearningTest.lean`](../GameTheory/Analysis/Protocol/BayesianZeroSumLearningTest.lean) | supported | Explicit-order serialization preserves canonical `IsεNash` at unchanged epsilon for arbitrary serialized profiles and translated source profiles. Qualifying sites also have generic local regret matching, bounded root decomposition, deviation-uniform root aggregation, and canonical fixed-strategy regret. One-site and same-depth multi-site two-player consumers reach approximate empirical Nash with moving laws and exact nonzero controls over complete contingent plans. Reusable scheduling, arbitrary behavioral replacements, and unequal-depth fibers remain separate. |
| Compile and observation-prune typed MAIDs while preserving laws and Nash | [`GameTheory/Languages/MAID.lean`](../GameTheory/Languages/MAID.lean), [`GameTheory/Languages/MAID/Strategic.lean`](../GameTheory/Languages/MAID/Strategic.lean), [`GameTheory/Languages/MAID/ObservationPruning.lean`](../GameTheory/Languages/MAID/ObservationPruning.lean), [`GameTheory/Tests/MAIDObservationPruning.lean`](../GameTheory/Tests/MAIDObservationPruning.lean), [`GameTheory/Tests/MAIDSafeReduction.lean`](../GameTheory/Tests/MAIDSafeReduction.lean), [`GameTheory/Tests/MAIDPruningComposition.lean`](../GameTheory/Tests/MAIDPruningComposition.lean), [`GameTheory/Experimental/PostArchitecture/MAIDPruningNonrelevantInvariance.lean`](../GameTheory/Experimental/PostArchitecture/MAIDPruningNonrelevantInvariance.lean), [`GameTheory/Experimental/PostArchitecture/MAIDPruningSiteReduction.lean`](../GameTheory/Experimental/PostArchitecture/MAIDPruningSiteReduction.lean), [`GameTheory/Experimental/PostArchitecture/MAIDStrategicNonreachability.lean`](../GameTheory/Experimental/PostArchitecture/MAIDStrategicNonreachability.lean), [`GameTheory/Experimental/PostArchitecture/MAIDPruningGlobalReduction.lean`](../GameTheory/Experimental/PostArchitecture/MAIDPruningGlobalReduction.lean), [`GameTheory/Experimental/PostArchitecture/MAIDPruningFixpointChecker.lean`](../GameTheory/Experimental/PostArchitecture/MAIDPruningFixpointChecker.lean), [`GameTheory/Experimental/PostArchitecture/MAIDPruningFixpointCheckerTest.lean`](../GameTheory/Experimental/PostArchitecture/MAIDPruningFixpointCheckerTest.lean) | opt-in | Native and compiled forms preserve canonical `IsεNash` at unchanged epsilon while one deviation replaces an owner's whole site-local policy family. Full-deviation coverage exactly characterizes safe Nash expansion, and already-certified nested reductions compose through relative coverage without recall; the two-signal control independently keeps coarse-to-full coverage while refuting the fine-to-coarse premise and Nash transfer. The experiment-only graphical chain now includes finite utility augmentation, one-site graphical ignorability, site-local optimality, one-source non-s-reachability transport under a fully mixed reference, source-first sufficient-recall induction from `SReachAcyclic` plus `IsEdgeAdditionFixpoint` to global `CoversFullDeviationsAt`, and an executable explicit-enumeration checker exactly equivalent to that fixpoint predicate. No stable automatic pruning pass, minimality/confluence theorem, or graph-predicate promotion follows; reopen those only for an independent consumer. |
| Model multi-round imperfect monitoring | [`GameTheory/Languages/MultiRound.lean`](../GameTheory/Languages/MultiRound.lean), [`GameTheory/Tests/MultiRoundMonitoring.lean`](../GameTheory/Tests/MultiRoundMonitoring.lean) | opt-in | Generic stagewise-Nash conveniences remain separate. |
| Solve intrinsic closed loops and analyze fixed-nature pure Nash | [`GameTheory/Languages/Intrinsic/Solution.lean`](../GameTheory/Languages/Intrinsic/Solution.lean), [`GameTheory/Languages/Intrinsic/Strategic.lean`](../GameTheory/Languages/Intrinsic/Strategic.lean), [`GameTheory/Tests/IntrinsicStrategic.lean`](../GameTheory/Tests/IntrinsicStrategic.lean) | opt-in | A deviation re-solves the whole configuration; nature lotteries, temporal execution, and behavioral/mixed strategy remain separate. |
| Compile Bayesian games through Protocol and transfer Nash | [`GameTheory/Languages/Bayesian/Strategic.lean`](../GameTheory/Languages/Bayesian/Strategic.lean), [`GameTheory/Tests/Bayesian.lean`](../GameTheory/Tests/Bayesian.lean) | opt-in | The language syntax remains solution-concept free; transfer lives in the strategic leaf. |
| Use Bayesian recommendation, truthful mechanisms, and revelation | [`GameTheory/Core/Bayesian.lean`](../GameTheory/Core/Bayesian.lean), [`GameTheory/Mechanism/BayesianIncentives.lean`](../GameTheory/Mechanism/BayesianIncentives.lean), [`GameTheory/Mechanism/Revelation.lean`](../GameTheory/Mechanism/Revelation.lean) | supported | Analytic envelope identities are not part of the stable API. |
| Use general Groves mechanisms, auctions, reserves, combinatorial allocation, and exact knapsack mechanisms | [`GameTheory/Mechanism/Groves.lean`](../GameTheory/Mechanism/Groves.lean), [`GameTheory/Tests/Groves.lean`](../GameTheory/Tests/Groves.lean), [`GameTheory/Tests/AuctionSemantics.lean`](../GameTheory/Tests/AuctionSemantics.lean) | opt-in | Public-choice and VCG consumers reach canonical DSIC; all-pay support is arithmetic only, and the greedy knapsack approximation has no truthfulness claim. |
| Implement target sets with nonnegative profile-observed transfers under weak undominance | [`GameTheory/Mechanism/Implementation.lean`](../GameTheory/Mechanism/Implementation.lean), [`GameTheory/Tests/Implementation.lean`](../GameTheory/Tests/Implementation.lean) | opt-in | Strategy profiles stay definitionally unchanged and payoff proofs use one additive-evaluation theorem; mixed, correlated, informational, price, and attainment extensions require separate consumers. |
| Use finite fair division, ordinal matching, and bargaining | [`GameTheory/Mechanism/FairDivision.lean`](../GameTheory/Mechanism/FairDivision.lean), [`GameTheory/Cooperative.lean`](../GameTheory/Cooperative.lean) | opt-in | Cake cutting, matching strategyproofness, and alternative bargaining solutions remain open. |
| Use compositional open-game machinery | none | frontier | Requires a compositional theorem and external semantic comparison before admission. |

The discriminating examples behind these claims are indexed in
[`SupportEvidenceMatrix.md`](SupportEvidenceMatrix.md).