IndisputableMonolith.Economics.MonetaryPolicyToolsFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Monetary Policy Tools from configDim — E6 Depth
   6
   7Five canonical central-bank monetary tools (= configDim D = 5):
   8  open-market operations, discount rate, reserve requirement,
   9  quantitative easing, forward guidance.
  10
  11Lean status: 0 sorry, 0 axiom.
  12-/
  13
  14namespace IndisputableMonolith.Economics.MonetaryPolicyToolsFromConfigDim
  15
  16inductive MonetaryTool where
  17  | openMarket
  18  | discountRate
  19  | reserveRequirement
  20  | qe
  21  | forwardGuidance
  22  deriving DecidableEq, Repr, BEq, Fintype
  23
  24theorem monetaryTool_count : Fintype.card MonetaryTool = 5 := by decide
  25
  26structure MonetaryToolsCert where
  27  five_tools : Fintype.card MonetaryTool = 5
  28
  29def monetaryToolsCert : MonetaryToolsCert where
  30  five_tools := monetaryTool_count
  31
  32end IndisputableMonolith.Economics.MonetaryPolicyToolsFromConfigDim
  33