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

horizonAtRung_strictly_decreasing

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)

  62theorem horizonAtRung_strictly_decreasing (k : ℕ) :
  63    horizonAtRung (k + 1) < horizonAtRung k := by

proof body

Tactic-mode proof.

  64  rw [horizonAtRung_succ_ratio]
  65  have hk : 0 < horizonAtRung k := horizonAtRung_pos k
  66  have hphi_inv_lt_one : phi⁻¹ < 1 := by
  67    have hphi_gt_one : (1 : ℝ) < phi := by
  68      have := Constants.phi_gt_onePointFive; linarith
  69    exact inv_lt_one_of_one_lt₀ hphi_gt_one
  70  have : horizonAtRung k * phi⁻¹ < horizonAtRung k * 1 :=
  71    mul_lt_mul_of_pos_left hphi_inv_lt_one hk
  72  simpa using this
  73

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.