eight_economic_phases
plain-language theorem explainer
The theorem establishes that economic phases equal eight when the octave is defined as eight ticks in RS-native units. Modelers of ledger-based business cycles aligned with the eight-tick evolution period cite this result to fix the phase count. The proof reduces the claim by unfolding the definitions of economicPhases, octave, and tick then normalizing the arithmetic.
Claim. Let economic phases be defined as octave divided by the fundamental tick. Then economic phases equals 8, where octave equals 8 times tick and tick equals 1 in RS-native units.
background
In the LedgerEconomics module economic phases are introduced as the ratio of the octave to the fundamental tick. The octave is the fundamental evolution period fixed at eight ticks, with tick as the RS time quantum set to one. This draws on the Constants module definition of octave as eight times tick and the MusicalScale definition of octave as the ratio two, together with the pulsar period construction as phi to the power k.
proof idea
The proof is a one-line wrapper that unfolds economicPhases as octave divided by tick, octave as eight times tick, and tick as one, then applies norm_num to obtain the equality to eight.
why it matters
The result embeds the T7 eight-tick octave directly into the economic ledger setting, supplying the phase count required by the forcing chain. It supports downstream constructions such as business cycle period and octave growth multiplier within the same module. No open scaffolding remains; the equality closes the phase enumeration for econ applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.