def definition def or abbrev

`p_max`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  66noncomputable def p_max : ℝ := hbar / l0

Definition body.

  67
  68/-- LHC maximum energy scale (in GeV). -/

From the project-wide theorem graph. These declarations reference this one in their body.

VacuumTestFalsifier in IndisputableMonolith.Flight.Falsifiers decl_use
costSpectrumValue_pow_general in IndisputableMonolith.NumberTheory.PrimeCostSpectrum decl_use
brillouinCutoff in IndisputableMonolith.QFT.UVCutoff decl_use
brillouin_equals_pmax in IndisputableMonolith.QFT.UVCutoff decl_use
cutoff_above_lhc in IndisputableMonolith.QFT.UVCutoff decl_use
rs_integral_finite in IndisputableMonolith.QFT.UVCutoff decl_use

Lean names referenced from this declaration's body.

l0 in IndisputableMonolith.Compat.Constants decl_use
hbar in IndisputableMonolith.Constants decl_use
hbar in IndisputableMonolith.Constants.Codata decl_use
scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
hbar in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
l0 in IndisputableMonolith.QFT.UVCutoff decl_use
hbar in IndisputableMonolith.Quantum.EntanglementEntropy decl_use