cycleDuration_pos
plain-language theorem explainer
The theorem establishes that the duration of the k-th business cycle on the phi-ladder is strictly positive for every natural number k. Economists working with RS-derived cycle models would cite it to confirm all predicted periods remain positive. The proof is a one-line wrapper that unfolds the explicit formula and invokes positivity of multiplication together with positivity of powers of the golden ratio.
Claim. For every natural number $k$, the cycle duration $4 phi^{2k}$ is strictly positive, where $phi$ is the golden ratio.
background
The module constructs a phi-ladder of business cycle durations in Recognition Science economics. Cycle durations are defined explicitly as $4 phi^{2k}$ for rung index $k$, producing the sequence that matches observed Kitchin (~4 y), Juglar (~10 y), and Kondratiev (~50 y) periods via successive factors of $phi^2$. The upstream definition cycleDuration(k) := 4 * phi^(2 * k) supplies the concrete expression; a parallel definition appears in the sociology module for civilization cycles. The local setting is Tier F Economics, which derives periodicity directly from the self-similar fixed point phi forced in the T0-T8 chain.
proof idea
This is a one-line wrapper proof. It unfolds the definition of cycleDuration to the product 4 * phi^(2*k), then applies the lemma mul_pos to the product of two positive reals, with the constant 4 shown positive by norm_num and the power shown positive by pow_pos using the fact phi_pos.
why it matters
The result supplies the duration_pos field required by the BusinessCycleCert structure that certifies the full RS business-cycle model. It closes the positivity obligation for the phi-ladder construction in economics, consistent with the self-similar fixed point phi from the forcing chain and the eight-tick octave. The parent is businessCycleCert in the same module, which also records the phi-squared ratio between adjacent cycles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.