module module high

`IndisputableMonolith.Economics.BusinessCyclePeriodFromGap45`

The module defines the Juglar cycle period as eight times the golden ratio phi in RS-native units. Cycle theorists and econophysicists cite it to tie observed business cycles to the eight-tick octave of the forcing chain. It is a definition module that introduces periods, positions, and band lemmas without proofs.

claimThe Juglar cycle period is given by $T_J = 8 phi$, where $phi$ denotes the self-similar fixed point of the Recognition Composition Law.

background

The module imports the RS time quantum tau_0 = 1 tick from Constants and cost functions from Cost. It introduces juglar_period as 8 phi, kondratieff_period, their positions on the phi-ladder, and consistency bands such as juglar_band and kondratieff_in_classical_band. The local setting is the T7 eight-tick octave of the UnifiedForcingChain, in which periods arise as integer multiples of the base tick scaled by phi.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Juglar and Kondratieff periods to the Recognition Science economics framework and feeds BusinessCyclePeriodCert. It realizes the T7 step of the forcing chain by mapping the eight-tick octave to the classical Juglar cycle length. It touches the derivation of empirical cycle periods from RS-native constants.

scope and limits

Does not derive the period from the full T0-T8 forcing chain.
Does not include empirical data fitting or validation.
Does not cover additional cycles such as Kitchin.
Does not prove consistency beyond the declared bands.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (14)

def juglar_period L53
def kondratieff_period L56
theorem juglar_pos L59
theorem kondratieff_pos L62
theorem juglar_band L68
theorem juglar_consistent_with_extended_band L77
theorem kondratieff_eq_45 L82
theorem kondratieff_in_classical_band L84
def schumpeter_ratio L91
theorem schumpeter_ratio_pos L93
theorem schumpeter_ratio_band L98
structure BusinessCyclePeriodCert L110
def businessCyclePeriodCert L117
theorem business_cycle_one_statement L128