pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Economics.GameTheoryFromRS

show as:
view Lean formalization →

The module derives game-theoretic notions from Recognition Science by characterizing Nash equilibrium as the vanishing of J-cost. Economists and physicists seeking a unified foundation for strategic behavior would cite it to link equilibria to the core J-equation. The module supplies type definitions and characterizations that rest directly on the imported Cost module.

claimIntroduces GameType as a structure for strategic interactions and certifies Nash equilibrium by the condition $J=0$.

background

Recognition Science starts from the single functional equation whose solutions yield the J-cost function satisfying the Recognition Composition Law. The module imports the Cost module, which supplies the definition of J-cost and its algebraic properties. It then introduces GameType to encode games and defines nash_equilibrium together with off_equilibrium and GameTheoryCert to mark the J=0 locus.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the interface that lets Recognition Science reach economics, feeding downstream models that treat strategic choice as a special case of J-cost minimization. It realizes the Nash condition directly from the J-uniqueness property in the forcing chain, closing one step toward deriving economic behavior from the single functional equation without additional postulates.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)