`p_max`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.QFT.UVCutoff on GitHub at line 66.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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 : ℝ
  91  dimension : ℕ := 4  -- 3 space + 1 time
  92
  93noncomputable def fundamentalLattice : VoxelLattice := { spacing := l0 }
  94
  95/-- On a lattice with spacing a, momenta are periodic with period 2π/a.
  96

papers checked against this theorem

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