J_bit_pos

formal source

  68    _ = cosh (log phi) - 1 := J_exp_eq_cosh (log phi)
  69
  70/-- J_bit > 0 since φ > 1 implies cosh(ln φ) > 1. -/
  71theorem J_bit_pos : J_bit_val > 0 := by
  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. -/
  80theorem J_bit_explicit : J_bit_val = (phi + phi⁻¹) / 2 - 1 := rfl
  81
  82/-- Using φ + 1/φ = φ + (φ - 1) = 2φ - 1 (from φ² = φ + 1 ⟹ 1/φ = φ - 1).
  83    Therefore J_bit = (2φ - 1)/2 - 1 = φ - 3/2.
  84
  85    **Note**: This is exact. 1/φ = φ - 1 (from φ² = φ + 1).
  86    So φ + 1/φ = 2φ - 1.
  87    J_bit = (2φ - 1)/2 - 1 = φ - 3/2 ≈ 1.618 - 1.5 = 0.118. -/
  88theorem J_bit_eq_phi_minus : J_bit_val = phi - 3/2 := by
  89  unfold J_bit_val J
  90  -- Key identity: 1/φ = φ - 1 (from φ² = φ + 1)
  91  have h_inv : phi⁻¹ = phi - 1 := by
  92    have hphi_ne : phi ≠ 0 := phi_pos.ne'
  93    have hsq : phi^2 = phi + 1 := phi_sq_eq
  94    have : phi * phi = phi + 1 := by rw [← sq]; exact hsq
  95    field_simp at this ⊢
  96    linarith
  97  rw [h_inv]
  98  ring
  99
 100/-- **Numerical Bound**: J_bit ≈ 0.118.
 101    Since 1.61 < φ < 1.62, we have 0.11 < J_bit < 0.12. -/