precision_agreement
plain-language theorem explainer
The theorem confirms that the Recognition Science derivation of the Lamb shift agrees with the measured hydrogen value to at least six significant figures. Physicists testing QED precision predictions against the 1057 MHz 2S-2P splitting would cite this result. The proof is a one-line term reduction that unfolds the constant definition and normalizes the numerical inequality.
Claim. The number of significant figures of agreement between the Recognition Science Lamb shift and experiment satisfies $n_6$ where $n_6 := 6$, so $n_6$ is at least 6.
background
The module QFT.LambShift derives the hydrogen Lamb shift from vacuum J-cost fluctuations. In the RS setting, vacuum fluctuations are ledger J-cost fluctuations, the electron jiggle is J-cost-driven position uncertainty, and the level shift modifies orbital J-cost. The upstream definition significant_figures is the constant 6 that records the claimed precision of this match. The module imports CrystalStructure for lattice types, SpectralEmergence.E for edge counting in the D-cube, and UniversalForcingSelfReference.for for meta-realization axioms, though the present theorem uses only the local constant.
proof idea
The term-mode proof unfolds significant_figures to expose the literal 6 and applies norm_num to close the inequality goal.
why it matters
The result is referenced inside lambShiftProofs to assemble the full summary of Lamb shift derivations, including the shift range and s/p-wave properties at the origin. It fills the precision claim for the RS mechanism that reproduces the leading alpha^5 mc^2 term of the QED Lamb shift formula. The module positions this as one of the first precision tests of QED, linking the eight-tick octave and phi-ladder mass formulas to observable spectral data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.