BusinessCyclePhase
plain-language theorem explainer
BusinessCyclePhase enumerates the five canonical phases of the economic cycle as an inductive type equipped with decidable equality and finite cardinality. An economist working in the phi-ladder model cites it when certifying counter-cyclical policy lengths tied to gap-45. The definition is a direct enumeration that installs the derived Fintype instance automatically.
Claim. The business cycle phases form the finite set $S = 5$ with elements $S = 5$ consisting of trough, recovery, expansion, peak, and contraction, equipped with decidable equality and finite type structure.
background
Recognition Science models economic cycles on the phi-ladder, with the Juglar cycle identified with approximately nine to eleven years and the Kondratieff wave fixed at gap-45 years. The module states that optimal counter-cyclical policy sets stimulus length to phi years in recession and austerity length to phi squared years in expansion, satisfying the balance condition stimulus over austerity equals phi inverse, with budget swings bounded by gap-45 percent of GDP. The five phases are presented as matching configDim equal to five.
proof idea
Direct inductive definition enumerating the five constructors, followed by a deriving clause that installs DecidableEq, Repr, BEq, and Fintype instances.
why it matters
The enumeration is required by the downstream theorem businessCyclePhaseCount establishing cardinality five and by the structure CounterCyclicalPolicyCert that records the Kondratieff period of forty-five together with the policy balance ratio. It fills the gap-45 step in the E6 economics chain, linking the five-phase cycle to the RS prediction of optimal policy swings. The construction is consistent with the self-similar fixed point phi and the forcing chain landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.