experimental_uncertainty
plain-language theorem explainer
Experimental uncertainty on the Lamb shift is fixed at the rational 29/10000 MHz. Researchers comparing Recognition Science J-cost derivations to QED measurements cite this constant to bound error in the 2S-2P splitting. The declaration is a direct constant assignment with no computation or lemmas.
Claim. The experimental uncertainty on the Lamb shift is $29/10000$ MHz.
background
The QFT module derives the Lamb shift from vacuum J-cost fluctuations, where J-cost tracks ledger imbalance via the functional equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). Electron jiggle from these fluctuations alters orbital J-cost and splits the nominally degenerate 2S_{1/2} and 2P_{1/2} levels. The module imports Constants and Cost to supply phi-based units and the J-cost definition but treats this uncertainty as an external experimental input.
proof idea
The declaration is a direct definition assigning the rational constant 29/10000.
why it matters
This constant feeds the downstream theorems theory_more_precise and uncertainties_small, which show theoretical uncertainty is smaller than experimental and both remain negligible relative to the shift. It anchors the QFT-012 claim that vacuum J-cost fluctuations reproduce the observed splitting with higher precision than measurement, linking T5 J-uniqueness and the phi-ladder to precision QED tests.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.