octaveGrowthMultiplier
plain-language theorem explainer
The octave growth multiplier is defined as φ raised to the eighth power. Economists modeling Recognition Science ledger cycles cite it when deriving bounds on 8-phase growth. It is introduced as a direct definition that inherits the algebraic identity φ^8 = 21φ + 13 from golden-ratio recurrence relations.
Claim. The octave growth multiplier equals $φ^8$, where $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
In the LedgerEconomics module, economic phases and business cycles are scaled by the eight-tick octave. Upstream, Constants.octave defines one octave as 8 ticks, the fundamental evolution period, while MusicalScale.octave supplies the frequency ratio 2. The constant φ enters as the self-similar fixed point from the forcing chain T6, with its powers appearing on the phi-ladder for growth formulas.
proof idea
This is a one-line definition that directly assigns phi raised to the power 8. It relies only on the imported phi from Constants and real exponentiation; no further lemmas are invoked.
why it matters
This definition supplies the growth factor for the theorem octaveGrowth_bounds, which proves the falsifiable interval (46, 48). It realizes the T7 eight-tick octave landmark, linking the period-8 evolution to economic phases via the Recognition Composition Law. The downstream result supplies a concrete test: empirical 8-year compounding outside this interval would refute the RS phi-scaling hypothesis for cycles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.