J_bit_eq_cosh

formal source

  60noncomputable def J_bit_val : ℝ := J phi
  61
  62/-- Alternative expression: J_bit = cosh(ln φ) - 1. -/
  63theorem J_bit_eq_cosh : J_bit_val = cosh (log phi) - 1 := by
  64  unfold J_bit_val
  65  have hphi : phi > 0 := phi_pos
  66  have h_exp_log : exp (log phi) = phi := exp_log hphi
  67  calc J phi = J (exp (log phi)) := by rw [h_exp_log]
  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