pith. machine review for the scientific record. sign in
theorem proved tactic proof

cycleDuration_succ_ratio

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  29theorem cycleDuration_succ_ratio (k : ℕ) :
  30    cycleDuration (k + 1) / cycleDuration k = phi ^ 2 := by

proof body

Tactic-mode proof.

  31  unfold cycleDuration
  32  have hphi_ne := phi_ne_zero
  33  have hphi_pos := phi_pos
  34  have h4phi : (4 * phi ^ (2 * k)) ≠ 0 := by
  35    exact (mul_pos (by norm_num) (pow_pos phi_pos _)).ne'
  36  rw [div_eq_iff h4phi]
  37  ring
  38

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.