lamb_shift_approx
plain-language theorem explainer
The declaration proves that the Lamb shift frequency in hydrogen lies strictly between 1057 and 1059 MHz. Researchers comparing Recognition Science derivations of vacuum J-cost fluctuations to experimental QED data would cite this numerical bound. The proof is a one-line term wrapper that unfolds the rational definition and discharges the inequalities by numerical normalization.
Claim. The Lamb shift frequency satisfies $1057 < 10578446/10000 < 1059$ in MHz units.
background
The module QFT-012 derives the Lamb shift from vacuum J-cost fluctuations in Recognition Science. The Lamb shift is the small energy splitting between the 2S_{1/2} and 2P_{1/2} levels of hydrogen, observed at approximately 1058 MHz. In the RS account, vacuum fluctuations appear as ledger J-cost fluctuations that induce electron position uncertainty and modify orbital J-cost. The upstream definition supplies the experimental rational 10578446/10000 as the concrete value of the shift in MHz. The scalar field constant from the relativity import is available but not invoked in this bound.
proof idea
The proof is a term-mode wrapper. It unfolds the definition of the Lamb shift in MHz, applies the constructor tactic to split the conjunction, and finishes both sides with norm_num to verify the numerical inequalities.
why it matters
This bound populates the shift_range field inside the LambShiftProofs structure that summarizes the Recognition Science treatment of the Lamb shift. It directly supports the QFT-012 target of obtaining the observed splitting from J-cost vacuum fluctuations, consistent with the phi-ladder and eight-tick octave in the broader forcing chain. The result touches the open question of how tightly the derived alpha band must match the experimental interval (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.