BehavioralFinding
plain-language theorem explainer
BehavioralFinding enumerates five standard behavioral biases as constructors of an inductive type inside the RS economics module. Modelers who derive agent behavior from J-cost would cite it to treat empirical biases as nonzero recognition defects. The declaration is a plain inductive definition that derives Fintype so downstream cardinality statements become decidable.
Claim. The inductive type of behavioral findings is generated by the five constructors loss aversion, anchoring, hyperbolic discounting, herding, and overconfidence.
background
The module sets configDim D = 5 and identifies the five findings with recognition error. Rational agents satisfy Jcost 1 = 0; any other ratio r yields Jcost r > 0. J-cost is the Recognition Science measure of systematic misrecognition of value, zero only for perfect recognition.
proof idea
The declaration is an inductive definition with exactly five cases, automatically deriving DecidableEq, Repr, BEq, and Fintype instances.
why it matters
It supplies the five findings required by BehavioralEconomicsCert, which asserts Fintype.card BehavioralFinding = 5 together with the rational and biased J-cost conditions. The definition realizes the module claim that these findings equal configDim D = 5 and thereby links behavioral data to the Recognition Composition Law and the phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.