businessCyclePeriodCert
plain-language theorem explainer
The declaration constructs a certificate bundling positivity, band membership, and ratio constraints for the Juglar and Kondratieff macroeconomic periods derived from recognition science. Researchers in cycle theory would cite it when linking empirical periods to the eight-tick cadence and gap-45 lattice. It is assembled as a direct structure construction referencing the component theorems for each field.
Claim. Let $T_J$ denote the Juglar period and $T_K$ the Kondratieff period. The certificate asserts $0 < T_J$, $12.8 < T_J < 13.0$, $T_K = 45$, $44 ≤ T_K ≤ 60$, and $3.4 < T_K/T_J < 3.6$.
background
The module derives macroeconomic cycle periods from the recognition science framework, specifically the eight-tick octave and the gap-45 on the inter-firm credit graph. The Juglar period is defined as eight times the golden ratio phi, yielding approximately 12.94 years, while the Kondratieff period is the bare gap value of 45 years. Upstream results establish the positivity of the Juglar period, its placement in the (12.8, 13.0) band, the exact equality of the Kondratieff period to 45, its containment in the classical 44-60 band, and the Schumpeter ratio in (3.4, 3.6). The local setting is Track I4 of Plan v5, treating these as direct consequences of RS primitives.
proof idea
The definition constructs the BusinessCyclePeriodCert structure by assigning each field to the corresponding sibling theorem: juglar_pos for positivity, juglar_band for the interval constraint, kondratieff_eq_45 for the exact value, kondratieff_in_classical_band for the wider interval, and schumpeter_ratio_band for the ratio constraint. It is a one-line wrapper that directly references these component results without additional reasoning.
why it matters
This declaration packages the derived periods for the business cycle into a single certifiable object, completing the derivation from the eight-tick recognition cadence and gap-45 lattice as described in the module documentation. It supports the claim that RS predicts the Juglar cycle at 8 phi and Kondratieff at 45 years, with the Schumpeter containment ratio matching historical reports. No downstream uses are recorded yet, but it closes the local theorem chain for economics applications of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.