BehavioralEconomicsCert
plain-language theorem explainer
BehavioralEconomicsCert packages the claim that exactly five behavioral findings exist under the RS cost function J, with rational agents at Jcost(1)=0 and biased agents satisfying Jcost(r)>0 for r≠1. Researchers in behavioral economics would reference it to embed the standard biases within Recognition Science. The declaration is a plain structure bundling the cardinality and the two Jcost axioms.
Claim. Let $J$ be the recognition cost function. The structure asserts that the set of behavioral findings has cardinality 5, that $J(1)=0$, and that $J(r)>0$ for all $r>0$ with $r≠1$.
background
The module identifies five canonical behavioral findings (loss aversion, anchoring, hyperbolic discounting, herding, overconfidence) with configuration dimension D=5. The inductive type BehavioralFinding enumerates exactly these five cases and derives Fintype, DecidableEq, and related instances. The J-cost function, imported from the Cost module, quantifies recognition error: it vanishes for perfect recognition and is positive for systematic error.
proof idea
The declaration is a structure definition that directly specifies the three fields: the cardinality of BehavioralFinding equals 5, Jcost at 1 equals 0, and Jcost is positive for all positive r not equal to 1.
why it matters
This certificate is instantiated in the downstream definition behavioralEconomicsCert, which supplies concrete values for the fields. It places the five behavioral findings inside the Recognition Science framework, where rational behavior corresponds to J=0 and bias to J>0, consistent with J-uniqueness in the forcing chain. It touches the open question of deriving specific bias magnitudes such as loss aversion λ≈φ² from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.