def definition def or abbrev

`cycleDuration`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  24noncomputable def cycleDuration (k : ℕ) : ℝ := 4 * phi ^ (2 * k)

Definition body.

From the project-wide theorem graph. These declarations reference this one in their body.

BusinessCycleCert in IndisputableMonolith.Economics.BusinessCycleFromPhiLadder decl_use
cycleDuration_pos in IndisputableMonolith.Economics.BusinessCycleFromPhiLadder decl_use
cycleDuration_succ_ratio in IndisputableMonolith.Economics.BusinessCycleFromPhiLadder decl_use
CivilizationCyclesCert in IndisputableMonolith.Sociology.CivilizationCyclesFromPhiLadder decl_use
cycleDuration in IndisputableMonolith.Sociology.CivilizationCyclesFromPhiLadder decl_use
cycleDurationRatio in IndisputableMonolith.Sociology.CivilizationCyclesFromPhiLadder decl_use

Lean names referenced from this declaration's body.

cycleDuration in IndisputableMonolith.Sociology.CivilizationCyclesFromPhiLadder decl_use