MarketMicrostructureCert
plain-language theorem explainer
The MarketMicrostructureCert structure asserts that the market microstructure model admits exactly five regimes by requiring the cardinality of the enumerated MarketRegime type to equal five. Economists working in the Recognition Science framework cite this when linking the J-cost functional to observable trading configurations. The definition is immediate from the Fintype instance on the five-constructor inductive type.
Claim. Let $R$ be the finite set of market regimes consisting of continuous double auction, periodic call auction, dealer market, dark pool, and high-frequency market. The structure MarketMicrostructureCert is the record type whose single field requires $|R| = 5$.
background
The module derives market microstructure from the J-cost functional in Recognition Science. It introduces five canonical regimes that correspond to configuration dimension five: continuous double auction, periodic call auction, dealer market, dark pool, and high-frequency market. These regimes are formalized as the constructors of the inductive type MarketRegime, which automatically derives DecidableEq, Repr, BEq, and Fintype.
proof idea
The declaration is a structure definition containing one field that states the cardinality of MarketRegime equals five. It relies directly on the Fintype instance derived from the inductive enumeration of exactly five cases. No lemmas or tactics are invoked beyond the automatic derivation.
why it matters
This definition supplies the certificate used by the downstream marketMicrostructureCert construction. It establishes the five-regime count in the E6 depth analysis of microstructure derived from J-cost, providing a concrete link to configuration dimension five. The structure closes a definitional step without axioms and supports further economic derivations in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.