MarketRegime
plain-language theorem explainer
MarketRegime enumerates five canonical market-microstructure configurations as an inductive type equipped with decidable equality and finite cardinality. Economists working in recognition-based models cite it when classifying trading mechanisms or establishing that exactly five regimes exist. The declaration is a direct enumeration whose only content is the five constructors plus the four derived typeclass instances.
Claim. Let $R$ be the finite set of market regimes consisting of the five elements: continuous double auction, periodic call auction, dealer market, dark pool, and high-frequency market.
background
The module Market Microstructure from J-Cost identifies five canonical regimes that realize configDim $D=5$ in the economics extension of Recognition Science. These regimes classify the discrete trading venues over which the J-cost functional equation is evaluated. The inductive definition supplies the carrier type for subsequent cardinality statements and certification structures.
proof idea
Direct inductive definition that lists the five constructors and immediately derives DecidableEq, Repr, BEq, and Fintype instances; no tactics or lemmas are applied beyond the deriving clause.
why it matters
MarketRegime is the type used by MarketMicrostructureCert (which asserts Fintype.card MarketRegime = 5) and by the marketRegime_count theorem. It supplies the discrete state space for the E6 depth layer, where the five regimes instantiate configDim $D=5$ and thereby extend the core forcing chain (T0–T8) into market microstructure. No open scaffolding remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.