AssetClass
plain-language theorem explainer
The inductive type enumerates the five canonical asset classes that fix the configuration dimension D equals 5 in the Recognition Science treatment of financial markets. Researchers extending the framework to economics cite this enumeration when they need a finite set on which to define J-cost equilibrium. The declaration is a direct inductive construction that derives decidable equality, representation, boolean equality, and finite-type structure automatically.
Claim. Let $A$ be the set whose elements are the five asset classes equities, bonds, commodities, currencies, and real estate, equipped with decidable equality and finite cardinality.
background
The module Financial Markets from RS identifies five canonical asset classes with the configuration dimension D = 5. In the Recognition Science setting, financial equilibrium is the condition J = 0, which recovers the efficient-market hypothesis; price deviations satisfy J > 0 and arbitrage opportunities are gaps that close toward J = 0. The inductive definition supplies the underlying finite set and automatically derives the instances DecidableEq, Repr, BEq, and Fintype from Mathlib.
proof idea
The declaration is a direct inductive definition with five constructors. No proof body is present; the deriving clauses for DecidableEq, Repr, BEq, and Fintype are supplied by the Lean compiler.
why it matters
This definition supplies the asset-class enumeration required by the downstream certification structure FinancialMarketsCert, which asserts that the cardinality of asset classes equals 5, the cardinality of financial risks equals 5, and Jcost 1 = 0. It realizes the module statement that five asset classes equal configDim D = 5 and thereby closes the economics extension of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.