pith. sign in
module module moderate

IndisputableMonolith.Economics.BehavioralEconomicsFromRS

show as:
view Lean formalization →

The module defines rational and biased agents in Recognition Science by tying agent type to J-cost from the Cost framework. Economists or RS modelers classifying decision makers under recognition constraints would cite the agent definitions and certification. It supplies named constants and a top-level certificate with no embedded proofs.

claimA rational agent satisfies $J=0$, where $J$ is the recognition cost function; a biased agent satisfies $J>0$. The module also supplies a certification object for behavioral findings derived from these agent types.

background

The module imports the Cost framework, which supplies the J-uniqueness function $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law. It introduces BehavioralFinding as a named economic observation and two agent predicates (rational_agent, biased_agent) that classify agents by whether their J-cost vanishes. The local setting is the direct translation of RS cost accounting into single-agent economic behavior.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the agent classification layer that BehavioralEconomicsCert uses to certify RS-derived behavioral findings. It occupies the interface between the J-cost primitives and economic applications of the Recognition Composition Law.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)