FinancialRisk
plain-language theorem explainer
FinancialRisk enumerates the five canonical risk categories that appear in the RS model of market equilibrium. Economists working inside the Recognition Science framework cite it when certifying that financial systems match configuration dimension D = 5. The declaration is a direct inductive definition that automatically derives the required type-class instances for decidability and finiteness.
Claim. Let $R$ be the set of financial risks. Then $R$ consists exactly of the five elements market risk, credit risk, liquidity risk, operational risk, and systemic risk.
background
The module treats financial markets as an instance of Recognition Science with five asset classes and five risk categories, both equal to the configuration dimension D. Equilibrium is defined by vanishing J-cost, J = 0, while positive J-cost signals price deviation and arbitrage opportunity. The inductive definition supplies the risk side of the certification that later enforces Fintype.card = 5 for both assets and risks.
proof idea
The declaration is a direct inductive definition that lists the five cases and derives DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters
It supplies the risk enumeration required by the FinancialMarketsCert structure, which also records Jcost 1 = 0. The definition completes the D = 5 matching for risks inside the RS economics module and links to the broader forcing chain in which configuration dimension is fixed at five for markets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.