MonetaryToolsCert
plain-language theorem explainer
MonetaryToolsCert is a structure whose single field requires the cardinality of the monetary tools type to equal five. Economists citing Recognition Science would reference it to confirm that the five standard central bank instruments match configDim D equals five. The definition is a direct structure whose field is discharged by the Fintype instance on the five-constructor inductive enumeration.
Claim. The structure $MonetaryToolsCert$ consists of a single field asserting that the cardinality of the set of monetary tools equals 5, where the monetary tools are the five cases open-market operations, discount rate, reserve requirement, quantitative easing, and forward guidance.
background
Recognition Science associates the configuration dimension D with five canonical monetary policy tools. The inductive type enumerates them explicitly as openMarket, discountRate, reserveRequirement, qe, and forwardGuidance, and derives DecidableEq, Repr, BEq, and Fintype instances so that its cardinality is immediately computable as 5.
proof idea
This is a structure definition. The sole field is satisfied directly by the cardinality value supplied by the Fintype instance on the five-constructor inductive type.
why it matters
The definition supplies the certified count that the downstream monetaryToolsCert instance consumes. It anchors the economics module to configDim D equals 5, consistent with the framework's derivation of D from the eight-tick octave in the forcing chain. No open questions or scaffolding are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.