marketMicrostructureCert
The definition supplies a concrete instance of the MarketMicrostructureCert structure by assigning the five-regime cardinality directly from the decided enumeration theorem. Economists working with J-cost dynamics in Recognition Science would cite it to fix the five canonical regimes as configDim D equals 5. The construction is a one-line field assignment that invokes the upstream cardinality result.
claimLet MarketRegime be the finite type whose five elements are the regimes continuous double auction, periodic call auction, dealer market, dark pool, and high-frequency market. The market-microstructure certificate is the structure whose five_regimes field satisfies Fintype.card(MarketRegime) = 5.
background
The module Market Microstructure from J-Cost establishes five canonical regimes that correspond to configDim D = 5 in the Recognition Science framework. MarketMicrostructureCert is the structure type whose sole field requires that the cardinality of MarketRegime equals 5. The upstream theorem marketRegime_count proves this equality by direct decision, supplying the concrete value used in the definition.
proof idea
The definition is a one-line wrapper that applies the marketRegime_count theorem by direct field assignment to the five_regimes slot of MarketMicrostructureCert.
why it matters in Recognition Science
This definition certifies the five-regime count inside the Economics module, anchoring the claim that configDim D equals 5 within the J-cost setting described in the module documentation. It supplies the verified cardinality that downstream economic models can reference when linking microstructure to the Recognition Composition Law and the phi-ladder. No parent theorems or open questions are recorded in the current dependency graph.
scope and limits
- Does not derive the five regime types from the J-cost functional equation.
- Does not prove stability or transitions among the regimes.
- Does not connect the cardinality result to the forcing chain T0-T8 or to constants such as alpha or G.
formal statement (Lean)
29def marketMicrostructureCert : MarketMicrostructureCert where
30 five_regimes := marketRegime_count
proof body
Definition body.
31
32end IndisputableMonolith.Economics.MarketMicrostructureFromJCost