businessCyclePeriod_upper
plain-language theorem explainer
The business cycle period in the Recognition Science ledger model satisfies a strict upper bound of 91 ticks. Economists using the phi-ladder for cycle calibration cite this result to constrain the length derived from the eight-tick octave. The proof reduces the claim algebraically by unfolding the period definition, substituting the closed form for phi to the fifth power, and applying a numerical inequality on phi.
Claim. The business cycle period $P$ satisfies $P < 91$.
background
The LedgerEconomics module constructs the business cycle period from the octave, defined as eight times the fundamental tick, and the golden ratio raised to the fifth power. The tick is the base time quantum equal to 1. Upstream lemmas provide the identity phi^5 = 5 phi + 3 and the bound phi < 1.62.
proof idea
The proof unfolds the business cycle period together with the definitions of octave and tick. It rewrites the resulting expression via the lemma phi_fifth_eq. The inequality is then discharged by nlinarith using the bound from phi_lt_onePointSixTwo.
why it matters
This upper bound combines with the lower bound to yield the full interval statement in businessCycle_bounds. It calibrates the economic cycle to the eight-tick octave from the UnifiedForcingChain and the phi-ladder. The result closes one link in the Recognition Science derivation of periodic economic phenomena from the core functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.