cycleDuration_succ_ratio
plain-language theorem explainer
The result shows that cycle durations increase by a factor of phi squared at each successive rung of the phi-ladder. Researchers modeling economic periodicity with golden-ratio scaling would invoke this to link Kitchin and Juglar cycles. The proof reduces the ratio to an algebraic identity after unfolding the explicit power-law formula and clearing the nonzero denominator.
Claim. For each natural number $k$, if $D(k) := 4 phi^{2k}$, then $D(k+1)/D(k) = phi^2$.
background
The module derives business cycle periods from the phi-ladder, with cycleDuration(k) defined as 4 times phi to the power 2k. This encodes the prediction that adjacent cycles scale by phi squared, reproducing observed durations of roughly 4, 10, and 50 years as described in the module documentation. The theorem relies on the upstream lemma phi_ne_zero, which states that phi is nonzero, together with the positivity of phi.
proof idea
The tactic proof first unfolds the definition of cycleDuration. It then obtains phi_ne_zero and phi_pos, constructs a proof that 4 * phi^(2*k) is nonzero, rewrites the division using div_eq_iff, and finishes with the ring tactic to verify the polynomial equality.
why it matters
This theorem populates the phi_sq_ratio component of businessCycleCert, the certification structure for the economic cycle model. It directly implements the phi-ladder scaling described in the module documentation, where the ratio phi^2 accounts for the progression from short inventory cycles to longer investment cycles. The result closes one link in the chain from the self-similar fixed point phi to observable economic timescales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.