J_exp_eq_cosh

formal source

  48theorem J_eq_Jcost (x : ℝ) : J x = Jcost x := rfl
  49
  50/-- J(exp t) = cosh(t) - 1 (the log-transformed version). -/
  51theorem J_exp_eq_cosh (t : ℝ) : J (exp t) = cosh t - 1 := by
  52  unfold J
  53  have h : (exp t)⁻¹ = exp (-t) := by simp [exp_neg]
  54  rw [h, Real.cosh_eq]
  55
  56/-- **Bit Cost**: J_bit := J(φ) = cosh(ln φ) - 1.
  57
  58This is the fundamental cost of a single ledger bit transition,
  59evaluated at the self-similar scale φ (golden ratio). -/
  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