pith. machine review for the scientific record. sign in
theorem proved term proof

hierarchy_very_small

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)

 189theorem hierarchy_very_small :
 190    hierarchyRatio < 1 / 10^16 := by

proof body

Term-mode proof.

 191  unfold hierarchyRatio higgsMassGeV planckMassGeV
 192  norm_num
 193
 194/-! ## Predictions and Tests -/
 195
 196/-- Testable predictions from RS UV cutoff:
 197
 198    1. **No trans-Planckian modes**: Physics is regular at Planck scale
 199    2. **Modified dispersion relations**: E² = p² + m² gets corrections at high p
 200    3. **Cosmic ray spectrum**: GZK cutoff might be modified
 201    4. **Black hole formation**: Minimum mass related to τ₀
 202    5. **Loop corrections**: Finite and calculable with RS cutoff -/

depends on (12)

Lean names referenced from this declaration's body.