businessCycleCert
plain-language theorem explainer
This definition builds a BusinessCycleCert record that certifies positive durations for all cycles on the phi-ladder together with the exact successor ratio phi squared. Economists working inside Recognition Science would cite it to anchor the predicted 4 y to 10 y to 50 y progression for Kitchin-Juglar-Kondratiev cycles. The construction is a direct record update that simply supplies the two required fields from the already-proved positivity and ratio lemmas.
Claim. The structure BusinessCycleCert is realized by the pair of statements: for every natural number $k$, $0 <$ cycleDuration$(k)$, and for every $k$, cycleDuration$(k+1)/$cycleDuration$(k) = phi^2$, where cycleDuration is the phi-ladder wavelength function.
background
The module models business-cycle periodicity inside Recognition Science by placing cycle durations on the phi-ladder, so that adjacent cycles are separated by two rungs and therefore stand in the ratio phi squared. BusinessCycleCert is the structure that packages the two minimal properties needed for this claim: universal positivity of the durations and the exact phi-squared successor ratio. The definition draws directly on the upstream theorems cycleDuration_pos (which unfolds the explicit form 4 * phi^(2*k) and invokes mul_pos together with pow_pos) and cycleDuration_succ_ratio (which performs the same unfolding followed by algebraic cancellation using phi_ne_zero and phi_pos).
proof idea
One-line wrapper that supplies the two fields of the BusinessCycleCert structure by direct reference to the theorems cycleDuration_pos and cycleDuration_succ_ratio.
why it matters
The definition closes the Tier F economics section by certifying the phi-ladder periodicity that the module doc-comment links to the observed Kitchin (~4 y), Juglar (~10 y) and Kondratiev (~50 y) cycles. It rests on the self-similar fixed point T6 and the Recognition Composition Law that forces the phi^2 ratio between successive rungs. No downstream theorems yet consume it, leaving open the question of embedding these cycle durations into a full macroeconomic model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.