IndisputableMonolith.Mathematics.GameTheoryDepthFromRS
Module packaging a finite enumeration of classical game-theoretic solution concepts and a certificate that their count matches a Recognition-Science depth prediction. Cited by anyone wiring combinatorial game theory into the RS forcing or certificate layer. Structure is definitional: an inductive (or listed) concept type, a cardinality lemma, and a cert record bundling the equality.
claimA finite type of classical solution concepts (Nash, subgame-perfect, etc.), together with a natural number equal to its cardinality, and a certificate asserting that this count equals the RS-predicted game-theory depth.
background
Recognition Science routinely packages discrete counts (ticks, dimensions, rung offsets) as small certificate records that pin a combinatorial fact to a forced integer from the T0–T8 chain. This module does the same for noncooperative game theory: it names a closed list of standard solution concepts and records how many there are.
The local objects are a solution-concept type, its cardinality as a natural number, and a GameTheoryDepthCert-style record that packages the equality between that count and the depth claimed by RS. Only Mathlib is imported; no analysis or measure theory is required.
Upstream forcing landmarks that motivate such certificates include the eight-tick octave (T7) and the discrete ladder structure used elsewhere for mass and coupling counts. The module itself stays purely combinatorial.
proof idea
Definition module with light proofs. A solution-concept enumeration is introduced, solutionConceptCount is obtained by Fintype.card (or an explicit list length), and gameTheoryDepthCert assembles a certificate record whose sole proof obligation is that the count equals the predicted depth integer. No analytic or fixed-point argument appears here.
why it matters in Recognition Science
Gives the RS stack a named, auditable handle on how many classical solution concepts are being counted when game theory is treated as a discrete depth layer. Downstream certificate aggregators and any theorem that quotes game-theory depth as an RS integer can import this module rather than re-listing concepts. It sits in the Mathematics domain alongside other depth-from-RS certificates and does not itself force Nash existence or refine equilibrium selection; it only locks the count.
scope and limits
- Does not prove existence or uniqueness of Nash (or any other) equilibrium.
- Does not derive the depth integer from T0–T8 inside this module.
- Does not treat cooperative, evolutionary, or continuum games.
- Does not connect solution concepts to the J-cost or RCL identities.
- Does not claim the enumerated list is exhaustive of all published refinements.