MonetaryTool
plain-language theorem explainer
The declaration introduces an inductive type enumerating five standard central-bank instruments as the concrete realization of configDim D = 5. Modelers in the Recognition Science economics layer cite the type to anchor the dimension of monetary-policy space. The definition is direct inductive construction with derived decidable equality, representation, and finite-type instances.
Claim. Let $M$ be the set whose elements are the five monetary-policy instruments: open-market operations, discount rate, reserve requirement, quantitative easing, and forward guidance. Equip $M$ with decidable equality and the structure of a finite type.
background
The module MonetaryPolicyToolsFromConfigDim fixes configDim D = 5 for the economics layer and enumerates the five canonical central-bank tools that realize this dimension. The inductive definition supplies the concrete carriers for openMarket, discountRate, reserveRequirement, qe, and forwardGuidance, together with the derived instances DecidableEq, Repr, BEq, and Fintype. No upstream lemmas are required; the definition stands alone as the base enumeration.
proof idea
The declaration is the inductive definition itself; no tactics or lemmas are applied. The five constructors are introduced directly and the derived instances are obtained automatically by the deriving clause.
why it matters
The type supplies the finite set whose cardinality is asserted by the downstream theorem monetaryTool_count and whose structure is packaged in the certificate MonetaryToolsCert. It therefore realizes the statement in the module documentation that five tools equal configDim D = 5, providing the concrete object on which later economic constructions in the Recognition framework rest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.