businessCyclePeriod
plain-language theorem explainer
The definition sets the business cycle period to eight times the fifth power of the golden ratio. Researchers deriving cycle lengths from the Recognition Science phi-ladder would cite this when bounding economic periods in ticks. It is a direct abbreviation that composes the imported octave constant with the phi^5 scaling.
Claim. The business cycle period equals $8 phi^5$, where the factor of eight is the fundamental octave period in ticks and $phi$ is the golden ratio.
background
The LedgerEconomics module extracts economic quantities from the Recognition Science forcing chain. The octave supplies the base period of eight ticks, matching the eight-tick octave forced at T7. The golden ratio $phi$ enters as the self-similar fixed point from T6 and appears in the mass formula and alpha-band scalings.
proof idea
This is a direct definition that multiplies the imported octave constant by $phi$ raised to the fifth power. It relies on the octave definitions from Constants (eight times the tick) and CoherenceExponent (two to the power D with D equal to three).
why it matters
This definition supplies the central scaling for business cycle analysis. It is used by the downstream theorems businessCycle_bounds, businessCyclePeriod_lower, and businessCyclePeriod_upper to establish the numerical interval (85, 91) in ticks. The construction instantiates the T7 eight-tick octave together with the phi^5 factor from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.