FinancialMarketsCert
plain-language theorem explainer
FinancialMarketsCert packages the Recognition Science assertion that markets operate with exactly five asset classes and five risk types under equilibrium at J-cost zero. Economists extending RS to finance would cite this to anchor efficient-market models in the J=0 condition. The structure is assembled directly from the Fintype cardinalities of the enumerated inductive types together with the equilibrium theorem imported from nonlinear dynamics.
Claim. A structure asserting that the set of asset classes (equities, bonds, commodities, currencies, real estate) has cardinality 5, the set of financial risks (market, credit, liquidity, operational, systemic) has cardinality 5, and the J-cost function satisfies $Jcost(1)=0$.
background
Recognition Science treats financial markets via a configuration dimension of 5. The module enumerates five asset classes (equities, bonds, commodities, currencies, real estate) and five risks (market, credit, liquidity, operational, systemic). Equilibrium is defined as the point where J-cost vanishes, corresponding to the efficient-market hypothesis in which price deviations close toward fair value.
proof idea
This is a structure definition with no proof body. It directly records the cardinality facts for the two inductive enumerations and invokes the upstream equilibrium result Jcost 1 = 0.
why it matters
The structure supplies the certificate type instantiated by financialMarketsCert. It embeds the RS claim that configDim equals 5 for both asset classes and risks, with equilibrium fixed at J=0, thereby linking the Recognition Composition Law and forcing chain to economic modeling. No open scaffolding remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.