pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Economics.BusinessCycleFromPhiLadder

show as:
view Lean formalization →

The module derives business cycle durations from the phi-ladder scaling within Recognition Science. It supplies cycleDuration together with positivity, ratio, and certification objects for economic periodicity. The structure is a sequence of definitions and elementary properties that rest on the base time quantum from Constants.

claimcycleDuration : ℕ → ℝ>0, cycleDuration_pos : ∀ n, cycleDuration n > 0, cycleDuration_succ_ratio : cycleDuration (n+1) / cycleDuration n = φ, BusinessCycleCert : Prop

background

Recognition Science obtains all scales from the J-functional fixed point phi after the forcing chain reaches T6. The imported Constants module fixes the RS time quantum as τ₀ = 1 tick. This economics module applies the same phi-ladder construction to generate discrete cycle lengths, with BusinessCycleCert serving as the interface that certifies a given duration belongs to the ladder.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the phi-ladder objects needed to extend the eight-tick octave (T7) into economic periodicity. It stands ready to feed any downstream theorem that invokes cycleDuration or BusinessCycleCert, although no such theorems are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)