planckMass

formal source

  38noncomputable def planckLength : ℝ := sqrt (hbar * G / c^3)
  39
  40/-- The Planck mass m_P = √(ℏc/G) ≈ 2.176 × 10⁻⁸ kg. -/
  41noncomputable def planckMass : ℝ := sqrt (hbar * c / G)
  42
  43/-- The Planck time t_P = √(ℏG/c⁵) ≈ 5.391 × 10⁻⁴⁴ s. -/
  44noncomputable def planckTime : ℝ := sqrt (hbar * G / c^5)
  45
  46/-- The Planck energy E_P = m_P c² ≈ 1.956 × 10⁹ J. -/
  47noncomputable def planckEnergy : ℝ := planckMass * c^2
  48
  49/-- The Planck temperature T_P = E_P / k_B ≈ 1.417 × 10³² K. -/
  50noncomputable def planckTemperature : ℝ := planckEnergy / (1.380649e-23)
  51
  52/-! ## Relationship to τ₀ -/
  53
  54/-- The ratio τ₀ / t_P:
  55
  56    τ₀ ≈ 1.288 × 10⁻²⁷ s
  57    t_P ≈ 5.391 × 10⁻⁴⁴ s
  58
  59    τ₀ / t_P ≈ 2.39 × 10¹⁶
  60
  61    This is a huge number! What powers of φ does it equal? -/
  62noncomputable def tau0_tP_ratio : ℝ := tau0 / planckTime
  63
  64/-- **ANALYSIS**: τ₀ / t_P ≈ 2.4 × 10¹⁶
  65
  66    log₁₀(2.4 × 10¹⁶) ≈ 16.4
  67    log_φ(10) = ln(10)/ln(φ) ≈ 4.785
  68
  69    So: log_φ(2.4 × 10¹⁶) ≈ 16.4 × 4.785 / 2.303 ≈ 34.0
  70
  71    Therefore: τ₀ / t_P ≈ φ³⁴