businessCyclePeriod_pos
plain-language theorem explainer
The Recognition Science ledger model sets the business cycle period to eight times the fifth power of the golden ratio in native ticks. Modelers of economic phases cite the result to guarantee all derived time scales remain positive. The proof reduces the definition via unfolding and applies a positivity tactic after invoking the golden-ratio positivity lemma.
Claim. $0 < 8 phi^5$, where $phi = (1 + sqrt(5))/2$ is the golden ratio and the prefactor 8 is the length of the fundamental octave in ticks.
background
The LedgerEconomics module constructs the business cycle period as the product of the octave and the fifth power of the golden ratio. The octave equals eight times the fundamental tick, the RS-native time quantum fixed at 1. This scaling inherits the eight-tick octave from the forcing chain and the phi-ladder used for periods and masses across modules.
proof idea
The proof is a one-line term-mode wrapper. It unfolds businessCyclePeriod, octave and tick to reach the explicit product 8 * phi^5, obtains the lemma phi_pos, and finishes with the positivity tactic.
why it matters
The declaration supplies the basic positivity needed for all subsequent economic-phase bounds and ledger ratios in the same module. It directly implements the eight-tick octave (T7) together with the phi^5 rung that appears in mass formulas and pulsar-period definitions. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.