pith. sign in
module module moderate

IndisputableMonolith.Economics.GameTheoryFromRS

show as:
view Lean formalization →

This module recasts game theory inside Recognition Science by identifying Nash equilibrium with vanishing J-cost. Economists and game theorists using RS foundations would cite the definitions and certificates. It consists of type and predicate definitions layered directly on the Cost module.

claimA strategy profile is a Nash equilibrium precisely when the recognition cost satisfies $J=0$.

background

The module imports the Cost framework, which supplies the J-cost function obeying the Recognition Composition Law. GameType classifies strategic situations while gameTheoryCert packages the equilibrium condition. The module doc states the central claim: Nash equilibrium: J = 0.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the bridge from Recognition Science to economics by equating Nash equilibrium to J=0. It extends the J-uniqueness result (T5) into multi-agent settings and supports further economic modeling, though no downstream theorems are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)