monetaryTool_count
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.