IndisputableMonolith.Economics.BehavioralEconomicsFromRS

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Behavioral Economics from RS — C Economics
   6
   7Five canonical behavioral economics findings (loss aversion, anchoring,
   8hyperbolic discounting, herding, overconfidence) = configDim D = 5.
   9
  10In RS: rational agent = J = 0 (perfect recognition of value).
  11Behavioral bias = J > 0 (systematic recognition error).
  12Loss aversion: λ ≈ φ² ≈ 2.618 (RS derivation).
  13
  14Lean: 5 findings.
  15
  16Lean status: 0 sorry, 0 axiom.
  17-/
  18
  19namespace IndisputableMonolith.Economics.BehavioralEconomicsFromRS
  20open Cost
  21
  22inductive BehavioralFinding where
  23  | lossAversion | anchoring | hyperbolicDiscounting | herding | overconfidence
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem behavioralFindingCount : Fintype.card BehavioralFinding = 5 := by decide
  27
  28/-- Rational agent: J = 0. -/
  29theorem rational_agent : Jcost 1 = 0 := Jcost_unit0
  30
  31/-- Biased agent: J > 0. -/
  32theorem biased_agent {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  33    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  34
  35structure BehavioralEconomicsCert where
  36  five_findings : Fintype.card BehavioralFinding = 5
  37  rational : Jcost 1 = 0
  38  biased : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  39
  40def behavioralEconomicsCert : BehavioralEconomicsCert where
  41  five_findings := behavioralFindingCount
  42  rational := rational_agent
  43  biased := biased_agent
  44
  45end IndisputableMonolith.Economics.BehavioralEconomicsFromRS
  46