lengthHierarchy
plain-language theorem explainer
lengthHierarchy enumerates the progression of length scales from the Planck cutoff through the RS voxel discreteness scale to proton and atomic sizes. Workers on quantum gravity cutoffs or discrete spacetime models cite the list when mapping the transition from recognition units to macroscopic physics. The declaration is a direct list definition that hardcodes the four string pairs with no reduction steps.
Claim. The length hierarchy is the ordered list of scales: Planck length $l_P approx 10^{-35}$ m (quantum gravity cutoff), voxel length $l_v approx 10^{-19}$ m (RS discreteness scale), proton size $approx 10^{-15}$ m, and atom size $approx 10^{-10}$ m.
background
The PlanckScale module derives Planck units from RS principles via the phi-ladder, where rung n satisfies tau_n = tau_0 * phi^{-n} and n=34 recovers the Planck time. The voxel marks the effective quantum gravity scale below which spacetime ceases to be well-defined. Upstream results supply the rung definition from Compat.Constants and the phi-powered scale function from Cosmology.LargeScaleStructureFromRS, both used to calibrate the listed tiers.
proof idea
Direct definition that constructs the List (String times String) by enumerating the four hardcoded pairs. No lemmas or tactics are invoked; the body is a literal list literal.
why it matters
The definition anchors the descriptive layer of QG-009 and QG-010 by exhibiting the hierarchy that links tau_0 to the Planck cutoff at phi-ladder rung 34. It supports the T5 J-uniqueness and T8 D=3 landmarks by making explicit the discrete-to-continuous transition inside the Recognition framework. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.