cycleDuration
plain-language theorem explainer
The definition assigns to each natural number k the real number 4 φ raised to 2k, where φ is the golden ratio. Economists modeling business cycles via Recognition Science cite it to generate the phi-ladder of durations for Kitchin, Juglar, and Kondratiev waves. The declaration is a direct one-line definition that doubles the exponent from the upstream sociology version and inserts the factor of 4 to enforce the observed phi-squared ratio between successive cycles.
Claim. The duration of the k-th business cycle is defined by the expression $4 φ^{2k}$, where $φ$ denotes the golden ratio.
background
Recognition Science places periodic economic phenomena on the phi-ladder, a self-similar sequence generated from the fixed point φ of the J-cost function. The upstream definition in Sociology.CivilizationCyclesFromPhiLadder.cycleDuration sets the base as φ^k. The module documentation states that adjacent cycle durations stand in the ratio φ² ≈ 2.618, reproducing the empirical sequence of short inventory cycles near 4 years, medium investment cycles near 10 years, and long structural cycles near 50 years.
proof idea
This is a direct definition that evaluates 4 multiplied by phi raised to twice the input index k. It imports the constant phi from Constants and aligns conceptually with the upstream sociology cycleDuration, but the body contains no further lemmas or tactics.
why it matters
The definition supplies the explicit formula certified by the BusinessCycleCert structure, which asserts positivity for every k and the exact ratio φ² between successive terms. It completes the economics tier of the phi-ladder predictions in the module documentation and feeds the related CivilizationCyclesCert in sociology. The construction rests on the self-similar fixed point φ from T6 of the forcing chain and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.