businessCyclePeriod_lower
plain-language theorem explainer
The theorem establishes that the business cycle period exceeds 85 ticks in the Recognition Science ledger model. Economists working with economic phases and ledger conservation would cite this bound to fix the cycle length on the phi-ladder. The proof reduces the period expression by unfolding its definition together with the octave and tick, rewrites via the phi fifth-power identity, and closes the inequality with nonlinear arithmetic on the lower bound phi > 1.61.
Claim. $85 < P$, where $P$ is the business cycle period in RS-native ticks, constructed as the product of the eight-tick octave and the fifth power of the golden ratio.
background
In the LedgerEconomics module the business cycle is placed on the phi-ladder using the fundamental time quantum tick (equal to 1) and the octave (equal to 8 ticks), the latter being the fundamental evolution period. The period itself is obtained by scaling the octave by phi^5, consistent with the period definition phi^k from the pulsar emission module. Upstream lemmas supply the exact identity phi^5 = 5 phi + 3 (from the Fibonacci recurrence) and the numerical fact phi > 1.61.
proof idea
The term proof unfolds businessCyclePeriod, octave and tick to obtain the concrete expression 8 * phi^5, rewrites the fifth power via the lemma phi_fifth_eq, and finishes with nlinarith applied to the hypothesis phi > 1.61 from phi_gt_onePointSixOne.
why it matters
The result supplies the lower conjunct of businessCycle_bounds, which asserts the full interval 85 < businessCyclePeriod < 91. It anchors the economic cycle to the eight-tick octave (T7) and the phi^5 rung, supporting the ledger conservation ratio and octave growth multiplier in the same module while linking to the pulsar period scaling phi^k.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.