pith. machine review for the scientific record. sign in
def definition def or abbrev

lengthHierarchy

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 101def lengthHierarchy : List (String × String) := [

proof body

Definition body.

 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)! -/

depends on (19)

Lean names referenced from this declaration's body.