lambShift_MHz
plain-language theorem explainer
This definition supplies the experimental Lamb shift frequency as the rational 1057.8446 MHz for Recognition Science QFT calculations. Researchers modeling vacuum J-cost fluctuations in hydrogen would cite the constant when anchoring numerical comparisons to spectroscopy data. The implementation is a direct rational literal assignment with no computation or external references.
Claim. The Lamb shift frequency is the rational number $1057.8446$ MHz, taken as the experimental value of the $2S_{1/2}$--$2P_{1/2}$ splitting in hydrogen.
background
The QFT.LambShift module derives the Lamb shift from vacuum J-cost fluctuations that modify orbital energies. The 2S state penetrates the nucleus while the 2P state is excluded, producing a small energy difference expressed in MHz. The local setting replaces standard QED vacuum polarization with ledger J-cost accounting built on upstream simplicial ledger and cost structures.
proof idea
The declaration is a direct constant definition assigning the rational literal 10578446/10000. No lemmas are applied and no tactics are used.
why it matters
The value feeds lamb_shift_approx, which proves the interval 1057 to 1059 MHz, and populates the LambShiftProofs structure confirming six-figure agreement and alpha^5 dependence. It anchors the RS claim that the shift originates in J-cost fluctuations, consistent with J-uniqueness and the RCL composition law in the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.