CounterCyclicalPolicyCert
plain-language theorem explainer
CounterCyclicalPolicyCert packages three conditions that certify a counter-cyclical policy model: five business cycle phases, a 45-year Kondratieff period, and a stimulus-to-austerity ratio of phi inverse. Economists working within Recognition Science would cite it to link phi-ladder predictions to concrete policy timings. The definition is a direct record of three independent conditions drawn from the module's supporting definitions.
Claim. A structure certifying that the business cycle has five phases, the Kondratieff wave equals 45 years, and the ratio of stimulus phase length to austerity phase length equals $phi^{-1}$.
background
The module defines five business cycle phases as trough, recovery, expansion, peak, and contraction. It sets the Kondratieff period to 45 years corresponding to gap-45 in the phi-ladder. Stimulus phase length is defined as phi years and austerity as phi squared years, with the policy balance theorem establishing their ratio as phi inverse.
proof idea
This declaration is a structure definition that directly assembles three field conditions from the module's supporting definitions and theorems. No tactics or lemmas are applied within the structure itself; the fields reference the inductive type BusinessCyclePhase, the constant kondratieffPeriod, and the theorem policy_balance.
why it matters
This structure provides the type for the concrete certificate counterCyclicalPolicyCert, which instantiates the conditions using businessCyclePhaseCount, reflexivity for the period, and the policy_balance theorem. It fills the gap-45 policy prediction step in the Economics module, linking the phi-ladder to economic cycle modeling. The five phases align with configDim D=5 as noted in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.