financialRiskCount
plain-language theorem explainer
Financial risk enumeration in RS yields exactly five categories. Market modelers cite this cardinality when building equilibrium certificates under the J=0 condition. The proof reduces to a decide tactic on the Fintype instance of the risk inductive type.
Claim. $|F| = 5$, where $F$ is the finite set of financial risks consisting of the five categories market, credit, liquidity, operational, and systemic.
background
The module treats financial markets via RS, with equilibrium defined by J-cost equal to zero. Five canonical financial risks are introduced and set equal to configuration dimension D = 5, matching the five asset classes. FinancialRisk is the inductive type enumerating precisely these five cases and deriving Fintype for direct cardinality computation. The upstream equilibrium theorem states that Jcost 1 = 0, supplying the J = 0 anchor for efficient-market translation.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. FinancialRisk derives DecidableEq and Fintype, so decide enumerates the five constructors and confirms the cardinality equals 5.
why it matters
This count supplies the five_risks field inside financialMarketsCert, which assembles the full market certification together with asset class count and the equilibrium condition. It realizes the module claim that five risks equal configDim D, anchoring the economics section to the Recognition Science framework where dimensions arise from the forcing chain. The declaration closes the enumeration with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.