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

predictions

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)

 203def predictions : List String := [

proof body

Definition body.

 204  "Dispersion relation corrections at E ~ E0",
 205  "Modified loop corrections near cutoff",
 206  "Finite quantum gravity effects",
 207  "Discrete spacetime effects in cosmology"
 208]
 209
 210/-! ## Comparison with Other Approaches -/
 211
 212/-- Other UV regularization approaches:
 213
 214    | Approach | Cutoff | Physical? |
 215    |----------|--------|-----------|
 216    | Dimensional reg | ε → 0 | No |
 217    | Pauli-Villars | Heavy mass M | Artificial |
 218    | Lattice QCD | Lattice spacing a | Physical on lattice |
 219    | String theory | String length l_s | Yes |
 220    | **RS** | τ₀ discreteness | **Yes, fundamental** |
 221
 222    RS is unique in providing a first-principles, non-arbitrary cutoff. -/

depends on (9)

Lean names referenced from this declaration's body.