lhcEnergyGeV
plain-language theorem explainer
lhcEnergyGeV fixes the LHC peak collision energy at 14000 GeV to benchmark the Recognition Science UV cutoff scale. Researchers comparing accelerator limits to discrete spacetime predictions would reference this constant when verifying that the natural cutoff lies well above current experimental reach. The definition consists of a direct rational assignment with no further computation or lemmas.
Claim. The LHC maximum energy scale is defined as $14000$ GeV.
background
The module QFT.UVCutoff derives the ultraviolet cutoff in quantum field theory from Recognition Science discreteness at the τ₀ scale, where momenta cannot exceed p_max = ℏ/τ₀. This supplies a first-principles regularization for otherwise divergent loop integrals. The upstream definition scale(k) := phi^k from LargeScaleStructureFromRS supplies the phi-ladder used to locate the cutoff energy relative to fundamental constants.
proof idea
The definition is a direct numeric assignment of 14000 to the rational type, with no lemmas or tactics applied.
why it matters
This constant feeds the theorem cutoff_above_lhc, which establishes that the RS UV cutoff exceeds LHC energies by more than 10^7. It anchors the comparison between the discrete spacetime cutoff and experimental scales in the QFT-013 framework, confirming that the natural regularization from information-theoretic discreteness operates far above current accelerator reach.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.