EconomicCycle
EconomicCycle enumerates five economic phases as an inductive type with automatic Fintype and DecidableEq instances. Cross-domain universality arguments cite it to place economic states inside the D=5 pattern shared by sensory, emotional, biological, and linguistic domains. The declaration is a direct inductive definition whose deriving clauses let decide compute cardinality five without further proof.
claimLet $E$ be the finite set of economic cycle phases $E = $ {recession, recovery, expansion, peak, contraction}, equipped with decidable equality and a Fintype structure of cardinality 5.
background
The module establishes that configDim D=5 occurs across independent domains in the Recognition Science framework, with HasConfigDim5 T defined to hold exactly when the cardinality of T equals 5. Five domain-specific types are supplied: SensoryModality, PrimaryEmotion, BiologicalState, EconomicCycle, and LinguisticRole. Each instance is verified by decide once the inductive type is declared with Fintype. The upstream peak definition from AsteroidOreSpectroscopy is not used in this declaration.
proof idea
Direct inductive definition introducing five constructors. The deriving clause for DecidableEq, Repr, BEq, and Fintype is discharged by Mathlib automation; the declaration contains no proof body.
why it matters in Recognition Science
EconomicCycle supplies the missing domain instance required by ConfigDimUniversalityCert and by the five_domain_product theorem that computes the 5^5 = 3125 cardinality of the full cross-domain product. It thereby supports the structural claim that D=5 appears with high frequency across the framework, consistent with the eight-tick octave and the earlier derivation of D=3 spatial dimensions in the forcing chain.
scope and limits
- Does not model transitions or dynamics among the five phases.
- Does not connect the phases to the J-cost function or phi-ladder.
- Does not assert that D=5 holds outside the five listed domains.
- Does not derive any physical constants or mass formulas from this type.
Lean usage
theorem economic_hasConfigDim5 : HasConfigDim5 EconomicCycle := by unfold HasConfigDim5; decideformal statement (Lean)
38inductive EconomicCycle where
39 | recession | recovery | expansion | peak | contraction
40 deriving DecidableEq, Repr, BEq, Fintype
41