juglar_band
plain-language theorem explainer
The theorem proves that the Juglar cycle period, defined as eight times the golden ratio, lies strictly between 12.8 and 13.0 years. Macroeconomic derivations within Recognition Science would cite this interval to match the 8-tick cadence to observed fixed-investment cycles. The proof unfolds the definition and reduces the claim to linear arithmetic on the established bounds 1.61 < phi < 1.62.
Claim. Let $T_J = 8 phi$. Then $12.8 < T_J < 13.0$.
background
The module derives business-cycle periods from the 8-tick recognition cadence and the gap-45 sigma-budget on the inter-firm credit graph. Juglar period is defined as eight times the golden ratio to absorb financial-sector latency, yielding approximately 12.94 years at the top of the empirical 7-11 yr band when expanded by a phi-credit factor. Upstream results supply the tight numerical bounds 1.61 < phi < 1.62 together with the definition of juglar_period itself.
proof idea
The term proof unfolds juglar_period to 8 * phi, invokes the lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo, then applies linarith twice to close the two-sided inequality.
why it matters
The bound is used directly by business_cycle_one_statement to assemble the full set of cycle claims and by the BusinessCyclePeriodCert structure. It supplies the concrete numerical content for the Juglar cycle predicted from the 8-tick octave and gap-45 in the Recognition Science framework, confirming consistency with the Schumpeter containment ratio near phi squared.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.