J

formal source

  42/-! ## Part 1: Bit Cost from the J Functional -/
  43
  44/-- The canonical cost functional J(x) = ½(x + x⁻¹) - 1. -/
  45noncomputable def J (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
  46
  47/-- J equals the standard Jcost. -/
  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