def
definition
planckLength
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Quantum.PlanckScale on GitHub at line 38.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
35/-! ## Planck Units -/
36
37/-- The Planck length l_P = √(ℏG/c³) ≈ 1.616 × 10⁻³⁵ m. -/
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