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

rung_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)

 301theorem rung_ratio (ys : ℝ) (hys : 0 < ys) (n : ℤ) :
 302    mass_rung ys (n + 1) / mass_rung ys n = phi := by

proof body

Term-mode proof.

 303  rw [mass_rung_step]
 304  have hmr : mass_rung ys n ≠ 0 := ne_of_gt (mass_rung_pos ys hys n)
 305  rw [mul_div_cancel_right₀ phi hmr]
 306
 307/-- **THEOREM**: The φ-ladder is self-similar: the ratio between
 308    ANY two rungs separated by k steps is φ^k. -/

depends on (9)

Lean names referenced from this declaration's body.