schumpeter_ratio_band
plain-language theorem explainer
The theorem establishes that the Schumpeter ratio, formed as the Kondratieff period divided by the Juglar period, lies strictly between 3.4 and 3.6. Economists tracing long-wave cycles to underlying lattice parameters would cite the bound to match Schumpeter's reported containment factor. The proof unfolds the three period definitions, invokes the tight golden-ratio bounds from the constants module, proves denominator positivity, and closes both sides with nlinarith after division rewriting.
Claim. $3.4 < 45/(8φ) < 3.6$, where φ denotes the golden ratio.
background
The module derives two dominant macroeconomic periods from the Recognition Science 8-tick cadence and the gap-45 lattice period on the inter-firm credit graph. Juglar period is defined as 8φ (8-tick scaled by the golden mean to absorb financial latency) and Kondratieff period as the bare gap value 45. Their ratio is the Schumpeter ratio, introduced to quantify the containment factor reported in Schumpeter 1939.
proof idea
The term proof unfolds schumpeter_ratio, juglar_period and kondratieff_period. It obtains the bounds 1.61 < φ < 1.62 from the constants module and establishes positivity of 8φ. Each target inequality is rewritten via lt_div_iff₀ or div_lt_iff₀ and discharged by nlinarith.
why it matters
The result supplies the final numerical bound required by the master statement business_cycle_one_statement in the same module, which packages the full set of cycle claims. It directly links the 8-tick octave and gap-45 primitives to the empirical Kondratieff-Juglar ratio. The bound closes the numerical verification step in Track I4 of the plan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.