behavioralFindingCount
plain-language theorem explainer
The theorem asserts that the inductive type enumerating canonical behavioral biases has cardinality exactly five. Economists applying Recognition Science to decision theory would cite this to fix the dimension of deviations from rational agents. The proof is a one-line decide tactic that computes the cardinality of the finite type whose five constructors are loss aversion, anchoring, hyperbolic discounting, herding, and overconfidence.
Claim. The set of behavioral findings has cardinality five: $ |B| = 5 $, where $ B $ is the finite set whose elements are loss aversion, anchoring, hyperbolic discounting, herding, and overconfidence.
background
The module Behavioral Economics from RS treats behavioral biases as positive J-cost, where J measures systematic recognition error relative to perfect value recognition (J = 0 for rational agents). The inductive type BehavioralFinding is defined with exactly five constructors: loss aversion (linked to λ ≈ φ²), anchoring, hyperbolic discounting, herding, and overconfidence. This enumeration is identified with configDim D = 5 in the Recognition Science setting.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the goal Fintype.card BehavioralFinding = 5. Because BehavioralFinding derives Fintype, decide exhaustively enumerates the five constructors and confirms the equality holds.
why it matters
This result supplies the five_findings component of the behavioralEconomicsCert definition, which packages the RS behavioral model. It directly realizes the module statement that five findings equal configDim D = 5, connecting to the Recognition Science forcing chain in which dimensions arise from the phi-ladder and J-uniqueness. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.