MonetaryTool
plain-language theorem explainer
The inductive definition enumerates the five canonical central bank instruments as the basis for the configDim equals five economic model. Researchers formalizing monetary policy inside the Recognition Science framework cite it to fix the finite set of tools before proving cardinality or certification properties. The definition proceeds by introducing one constructor per instrument and deriving the decidable equality and finite type instances automatically.
Claim. Let $T$ be the set of monetary policy tools. Then $T$ is the inductive type whose elements are open-market operations, discount rate, reserve requirement, quantitative easing, and forward guidance.
background
The module treats monetary policy tools as the concrete realization of configDim D equals 5 inside the Recognition Science economic layer. This dimension counts the independent instruments a central bank can deploy. The local theoretical setting is the five-tool enumeration that precedes any cardinality or certification statements in the same file.
proof idea
The declaration is the inductive definition itself. It lists the five constructors and lets Lean synthesize the DecidableEq, Repr, BEq, and Fintype instances with no additional lemmas or tactics required.
why it matters
It supplies the enumerated type whose cardinality is asserted equal to five by the downstream cardinality theorem and whose structure is packaged inside the certification record. The definition therefore anchors the claim that monetary policy lives in a five-dimensional configuration space, consistent with the framework's separation of spatial dimension three from economic configuration dimension five.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.