marketRegime_count
plain-language theorem explainer
The declaration asserts that the inductive type enumerating market regimes has cardinality exactly five. Researchers modeling market microstructure within Recognition Science cite this result to anchor the configuration dimension at five. The proof is a one-line decision procedure that exhausts the constructors of the finite inductive type.
Claim. The finite type of market regimes has cardinality five: $|M| = 5$, where $M$ consists of the regimes continuous double auction, periodic call auction, dealer market, dark pool, and high-frequency market.
background
The module derives market microstructure from J-cost and enumerates five canonical regimes that fix the configuration dimension at five. MarketRegime is the inductive type whose constructors are precisely those five regimes. The upstream inductive definition supplies the finite set whose cardinality is asserted here.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic computes the Fintype cardinality by enumerating the five constructors of the inductive type MarketRegime.
why it matters
This result supplies the five_regimes field of marketMicrostructureCert, which certifies the regime list in the economics module. It fills the step that sets configDim D = 5 in the derivation of market microstructure from J-cost. The theorem anchors the five-regime taxonomy used in downstream economic applications of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.