`l0`

definition

show as: view math explainer →

module: IndisputableMonolith.QFT.UVCutoff
domain: QFT
line: 60 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.UVCutoff on GitHub at line 60.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  57    This also determines:
  58    - Energy scale: E0 = hbar / tau0 ~ 5.1e-8 J ~ 3.2e11 GeV
  59    - Momentum scale: p0 = hbar / l0 ~ 1.7e-10 kg*m/s -/
  60noncomputable def l0 : ℝ := c * tau0
  61
  62/-- The fundamental energy scale. -/
  63noncomputable def E0 : ℝ := hbar / tau0
  64
  65/-- The fundamental momentum cutoff. -/
  66noncomputable def p_max : ℝ := hbar / l0
  67
  68/-- LHC maximum energy scale (in GeV). -/
  69def lhcEnergyGeV : ℚ := 14000  -- 14 TeV = 14000 GeV
  70
  71/-- RS cutoff energy scale (in GeV, approximate). -/
  72def rsCutoffGeV : ℚ := 3.2e11  -- ~320 billion GeV
  73
  74/-- **THEOREM**: The RS UV cutoff is ~10⁷ times higher than LHC energies. -/
  75theorem cutoff_above_lhc :
  76    rsCutoffGeV / lhcEnergyGeV > 10000000 := by
  77  unfold rsCutoffGeV lhcEnergyGeV
  78  norm_num
  79
  80/-! ## Discreteness and the Lattice -/
  81
  82/-- Spacetime is fundamentally discrete in RS.
  83
  84    The "voxel lattice" has spacing l₀ = c × τ₀.
  85
  86    On a lattice, momenta are bounded:
  87    - Maximum momentum: p_max = π ℏ / l₀
  88    - Brillouin zone: |p| < p_max -/
  89structure VoxelLattice where
  90  spacing : ℝ

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.