BusinessCycleCert
plain-language theorem explainer
BusinessCycleCert packages two universal properties of the cycle duration function on the phi-ladder: strict positivity for every natural number k and exact phi-squared scaling between successive terms. Economists working within Recognition Science would cite the structure when certifying the predicted wavelength ratios for Kitchin, Juglar and Kondratiev cycles. The declaration is a bare structure definition whose fields directly reference the upstream cycleDuration definition and require no further lemmas.
Claim. Let $d(k) = 4 phi^{2k}$ denote the cycle duration function. The structure BusinessCycleCert consists of the two assertions that $d(k) > 0$ for all natural numbers $k$ and that $d(k+1)/d(k) = phi^2$ for all $k$.
background
The module Economics.BusinessCycleFromPhiLadder models business-cycle wavelengths as a phi-ladder in which adjacent durations differ by two rungs, hence scale by phi squared. The function cycleDuration is introduced as the noncomputable definition $4 * phi^(2*k)$, chosen so that the k=0 term recovers the observed Kitchin inventory cycle of roughly four years. An independent but analogous cycleDuration appears in the sociology module as phi^k, confirming that the same scaling law governs both economic and civilizational periodicities. The module documentation states that this yields the observed sequence 4 y, 10.47 y, 50 y for the three classical cycle classes.
proof idea
The declaration is a structure definition with two fields, each a universal quantification over the cycleDuration definition. No tactics, lemmas or reduction steps are applied; the structure simply records the two required properties as its inhabitants.
why it matters
BusinessCycleCert supplies the type for the downstream businessCycleCert definition that instantiates the fields with the lemmas cycleDuration_pos and cycleDuration_succ_ratio. It therefore anchors the RS claim that economic cycle durations obey the same self-similar fixed point phi that appears in T6 of the forcing chain and in the Recognition Composition Law. The structure closes the gap between the abstract phi-ladder and the concrete numerical predictions for observed business-cycle periods.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.