theoretical_uncertainty
plain-language theorem explainer
The declaration supplies the fixed theoretical uncertainty bound of 0.0010 MHz for the Lamb shift frequency in the Recognition Science QFT derivation. Precision tests of QED and RS vacuum-fluctuation models cite this constant when confirming that the computed shift exceeds both experimental and theoretical error bars. It is introduced as a direct rational constant assignment with no reduction steps.
Claim. The theoretical uncertainty on the Lamb shift frequency is defined as the rational constant $0.0010$ MHz.
background
The QFT.LambShift module derives the 1057 MHz splitting between the 2S_{1/2} and 2P_{1/2} hydrogen levels from vacuum J-cost fluctuations. In this setting the electron experiences position uncertainty driven by ledger J-cost, which modifies the orbital J-cost and lifts the degeneracy that would otherwise hold without QED. The module imports structures ensuring collision-free empirical programs and simplicial edge lengths from psi, together with mechanism-design and mock-theta constructions that guarantee structural neutrality in the eight-tick framework.
proof idea
The definition is a direct rational assignment of the constant 10/10000. No lemmas are applied; the value is supplied as a fixed input for the downstream comparison theorems.
why it matters
This bound is invoked by the theorem theory_more_precise, which establishes that theoretical uncertainty is strictly smaller than experimental uncertainty, and by uncertainties_small, which shows both error bars are negligible relative to the Lamb shift magnitude. It thereby supports the RS claim that the shift arises from J-cost fluctuations with precision consistent with the phi-ladder and T5 J-uniqueness. No open scaffolding questions are closed by this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.