octaveGrowth_bounds
plain-language theorem explainer
Economists modeling business cycles under Recognition Science cite the strict inequality 46 < φ^8 < 48 on the octave growth multiplier. This supplies a concrete numerical window for eight-year compounding under the eight-tick octave. The term proof unfolds the multiplier definition, rewrites via the Fibonacci identity for φ^8, and closes both sides with nonlinear arithmetic on the supplied phi bounds.
Claim. $46 < φ^8 < 48$ where $φ$ is the golden ratio.
background
In LedgerEconomics the octave growth multiplier is defined as φ^8 and represents the compounding factor across eight economic phases. The upstream period definition sets period(k) := φ^k, linking the same scaling to astrophysical regimes. The identity φ^8 = 21φ + 13 follows from the Fibonacci recurrence. Separate lemmas give the tight bounds 1.61 < φ and φ < 1.62. The local setting translates the eight-tick octave (T7) and phi self-similar fixed point into ledger observables.
proof idea
Unfold octaveGrowthMultiplier to φ^8. Rewrite using phi_eighth_eq. Split the conjunction. Apply nlinarith to each inequality using the respective phi bound lemmas.
why it matters
The bound supplies the numerical content of the falsifiable prediction for phi-scaling in economic cycles. It realizes the T7 eight-tick octave landmark by producing the concrete interval (46,48) for the growth factor. No immediate parent theorems appear in the used_by list, yet the bound directly constrains business cycle period definitions in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.