pith. sign in
module module high

IndisputableMonolith.Economics.BehavioralEconomicsFromRS

show as:
view Lean formalization →

This module defines behavioral economics objects from Recognition Science by setting rational agents to J-cost zero and biased agents to positive J-cost. Decision theorists and economists modeling bounded rationality would cite it for the RS-native grounding of agent types. The module is built from definitions and a certification theorem on top of the imported Cost module.

claimRational agent: $J=0$; biased agent: $J>0$. BehavioralFinding enumerates deviations; BehavioralEconomicsCert certifies the resulting agent classification.

background

The module imports the J-cost definition from IndisputableMonolith.Cost, where J(x) = (x + x^{-1})/2 - 1 measures recognition defect. It introduces BehavioralFinding as a type of deviation from J=0 and behavioralFindingCount as its cardinality. The local setting extends the Recognition Composition Law and phi-ladder to economic agents, treating J=0 as the rational fixed point.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the agent taxonomy that feeds BehavioralEconomicsCert and downstream economic applications of the J-uniqueness (T5) and eight-tick structure. It closes the step from the Cost module to behavioral findings without introducing new forcing-chain hypotheses.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)