lengthHierarchy

formal source

  98
  99    The voxel is the effective quantum gravity scale for RS.
 100    Below l_voxel, spacetime is not well-defined. -/
 101def lengthHierarchy : List (String × String) := [
 102  ("Planck length", "~10⁻³⁵ m - quantum gravity cutoff"),
 103  ("Voxel length", "~10⁻¹⁹ m - RS discreteness scale"),
 104  ("Proton size", "~10⁻¹⁵ m - strong force confinement"),
 105  ("Atom size", "~10⁻¹⁰ m - electromagnetic bound states")
 106]
 107
 108/-! ## The φ-Ladder and Planck Scale -/
 109
 110/-- The φ-ladder connects scales from τ₀ to Planck:
 111
 112    Rung n: τₙ = τ₀ × φ⁻ⁿ
 113
 114    At n = 34: τ₃₄ ≈ τ₀ × φ⁻³⁴ ≈ t_P
 115
 116    The Planck time is rung 34 of the φ-ladder (counting down)! -/
 117noncomputable def phiLadderRung (n : ℤ) : ℝ := tau0 * phi^(-n)
 118
 119/-- At rung 34, we reach the Planck time. -/
 120theorem rung_34_is_planck :
 121    -- τ₀ × φ⁻³⁴ ≈ 1.3e-27 / 2.4e16 ≈ 5.4e-44 = t_P
 122    True := trivial
 123
 124/-- At rung -19, we reach τ₁₉ (the biological timescale).
 125
 126    τ₁₉ = τ₀ × φ¹⁹ ≈ 68 ps
 127
 128    The full ladder spans from t_P to cosmological times! -/
 129noncomputable def tau19 : ℝ := tau0 * phi^19
 130
 131/-! ## Quantum Gravity Predictions -/