monetaryTool_count
The theorem states that the inductive type enumerating five central-bank instruments has cardinality exactly five. Modelers of monetary policy inside the Recognition Science framework cite it to fix the configuration dimension at five. The proof is a one-line decide tactic that evaluates the automatically derived Fintype instance on the inductive definition.
claimThe finite type of monetary policy tools satisfies $ |MonetaryTool| = 5 $.
background
The module introduces MonetaryTool as an inductive type whose five constructors are openMarket, discountRate, reserveRequirement, qe and forwardGuidance; the type derives DecidableEq, Repr, BEq and Fintype. Module documentation identifies these five constructors with the canonical central-bank tools and equates them to configDim D = 5. The sole upstream dependency is the inductive definition itself, which supplies the Fintype instance required for the cardinality computation.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype.card expression; decide succeeds because the inductive type carries a derived Fintype instance whose cardinality is known at compile time.
why it matters in Recognition Science
The result populates the five_tools field of the downstream monetaryToolsCert definition. It supplies the concrete count that realizes configDim = 5 inside the economics module, aligning with the framework's use of configuration dimensions. No open questions or scaffolding are indicated in the supplied material.
scope and limits
- Does not derive the five tools from Recognition Science axioms.
- Does not model interactions or effectiveness of the tools.
- Does not admit additional instruments beyond the listed five.
Lean usage
def monetaryToolsCert : MonetaryToolsCert where five_tools := monetaryTool_countformal statement (Lean)
24theorem monetaryTool_count : Fintype.card MonetaryTool = 5 := by decide
proof body
25