EconomicCycle
plain-language theorem explainer
EconomicCycle enumerates five phases of an economic cycle as an inductive type. Cross-domain proofs in Recognition Science cite it to establish uniform cardinality 5 across sensory, emotional, biological, economic and linguistic domains. The declaration is a plain inductive definition that derives Fintype, DecidableEq and related instances automatically.
Claim. Let $EconomicCycle$ be the inductive type generated by the five constructors recession, recovery, expansion, peak and contraction.
background
Module C13 formalises configDim universality: the predicate HasConfigDim5 (T : Type) holds precisely when the finite cardinality of T equals 5. Five domain types are supplied, each proved to satisfy the predicate by decide. EconomicCycle supplies the economic instance. The module import brings in the unrelated peak frequency function from asteroid spectroscopy; that definition is not referenced by the inductive declaration itself.
proof idea
The declaration is an inductive definition with exactly five constructors. Deriving Fintype, DecidableEq, Repr and BEq equips the type with the required structure for later cardinality arguments; no tactics or lemmas are applied inside the declaration.
why it matters
EconomicCycle populates the ConfigDimUniversalityCert structure and is invoked by economic_hasConfigDim5 and five_domain_product. The latter shows that the product of the five D=5 domains has cardinality 3125. This supplies one concrete witness for the structural claim that configDim = 5 appears with high frequency across the framework, consistent with the eight-tick octave and the cross-domain product constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.