assetClassCount
plain-language theorem explainer
The theorem states that the Recognition Science financial model contains exactly five asset classes. Researchers verifying dimensional consistency between asset classes and risks in the J=0 equilibrium setting would cite this count. The proof reduces to a direct decidable computation on the enumerated inductive type.
Claim. The finite type of asset classes has cardinality five: $|AssetClass| = 5$, where AssetClass enumerates equities, bonds, commodities, currencies, and real estate.
background
The Financial Markets from RS module models financial equilibrium as the condition J = 0 under the Recognition Science J-cost, with price deviations corresponding to J > 0. AssetClass is defined as an inductive type with five explicit constructors that instantiate the configuration dimension D = 5, matching the five canonical financial risks also introduced in the module. The upstream AssetClass inductive supplies the finite, decidable structure that permits the cardinality statement.
proof idea
The proof is a one-line wrapper that applies the decide tactic to Fintype.card AssetClass = 5, which succeeds by exhaustive enumeration of the five constructors in the inductive definition.
why it matters
This result supplies the five_classes field inside the financialMarketsCert definition that certifies the RS-derived market structure. It realizes configDim D = 5 for the economics domain, consistent with the module's identification of five asset classes and five risks under the J = 0 equilibrium. No open questions or scaffolding are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.