businessCycle_bounds
plain-language theorem explainer
The theorem proves that the Recognition Science business cycle period, scaled as eight times phi to the fifth, lies strictly between 85 and 91 ticks. Ledger economists working in the Recognition framework cite this interval when calibrating phase durations or growth multipliers from the phi-ladder. The proof is a one-line term that directly conjoins the separately established lower and upper bounds.
Claim. $85 < 8 phi^5 < 91$, where $phi$ denotes the golden ratio and the period is expressed in Recognition ticks.
background
In the LedgerEconomics module the business cycle period is defined as the product of the eight-tick octave and phi raised to the fifth power. This follows the Recognition Composition Law and the eight-tick octave forced at step T7 of the UnifiedForcingChain. The lower bound theorem unfolds the definition, rewrites via the phi-fifth equation, and applies nlinarith with phi greater than 1.618; the upper bound does likewise with phi less than 1.62.
proof idea
The proof is the term pairing businessCyclePeriod_lower with businessCyclePeriod_upper. Each supporting theorem unfolds the definition of businessCyclePeriod, substitutes the phi-fifth identity, and closes the inequality by nlinarith on the supplied phi bounds.
why it matters
The bound fixes the business cycle duration inside a narrow window around 88.7 ticks, consistent with phi-ladder scaling. It supports sibling constructions such as eight_economic_phases and octaveGrowth_bounds. The result aligns with T7 (eight-tick octave) and the phi^5 factor used in the mass formula and constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.