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

J_bit_pos

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)

  71theorem J_bit_pos : J_bit_val > 0 := by

proof body

Term-mode proof.

  72  rw [J_bit_eq_cosh]
  73  have hphi : phi > 1 := one_lt_phi
  74  have h_log_pos : log phi > 0 := log_pos hphi
  75  -- one_lt_cosh : 1 < cosh x ↔ x ≠ 0
  76  have h_cosh_gt : 1 < cosh (log phi) := Real.one_lt_cosh.mpr h_log_pos.ne'
  77  linarith
  78
  79/-- Explicit formula: J_bit = ½(φ + φ⁻¹) - 1 = ½(φ + 1/φ) - 1. -/

used by (7)

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

depends on (8)

Lean names referenced from this declaration's body.