financialMarketsCert
plain-language theorem explainer
Financial markets in Recognition Science receive a certificate asserting exactly five asset classes, five risk categories, and vanishing J-cost at unit scale. An economist embedding efficient-market behavior inside the RS cost framework would cite this to ground the J = 0 equilibrium condition. The definition is a direct record constructor that substitutes the cardinality theorems and the base Jcost lemma into the three fields.
Claim. The financial markets certificate is the structure asserting that the cardinality of asset classes equals five, the cardinality of financial risk types equals five, and the J-cost function evaluated at unit scale equals zero.
background
Recognition Science measures deviation from equilibrium by the J-cost function, with the base property that Jcost 1 = 0. The module treats five canonical asset classes (equities, bonds, commodities, currencies, real estate) as the configuration dimension D = 5 and likewise identifies five canonical financial risks. The upstream theorems assetClassCount and financialRiskCount establish these cardinalities by decision procedures, while market_equilibrium reduces directly to the unit equilibrium lemma Jcost_unit0 imported from nonlinear dynamics.
proof idea
The definition is a direct structure constructor. It populates the five_classes field with assetClassCount, the five_risks field with financialRiskCount, and the equilibrium field with market_equilibrium.
why it matters
This definition supplies the concrete instance of the FinancialMarketsCert structure that realizes the RS account of financial markets at equilibrium J = 0. It completes the E4 economics section by linking the five-dimensional configuration to the J-cost vanishing condition. No downstream theorems yet depend on it, leaving open its use in derivations of price dynamics or arbitrage closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.