significant_figures
plain-language theorem explainer
Recognition Science sets the Lamb shift agreement threshold at six significant figures. Precision QED researchers cite this constant when confirming that the J-cost fluctuation model reproduces the measured 1057.8 MHz splitting. The definition is a direct natural-number assignment requiring no reduction or lemmas.
Claim. The number of significant figures to which the Recognition Science Lamb-shift prediction agrees with experiment is defined as $6$.
background
The module derives the Lamb shift from vacuum J-cost fluctuations, where ledger J-cost fluctuations produce the electron jiggle that lifts the 2S level above the 2P level. J-cost is the Recognition Science cost function satisfying the composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The module imports Constants and Cost to supply the numerical yardstick and phi-ladder values used in the shift calculation.
proof idea
The definition directly assigns the constant 6. The downstream precision_agreement theorem unfolds significant_figures and applies norm_num to discharge the inequality significant_figures ≥ 6.
why it matters
The constant supplies the precision clause inside the LambShiftProofs structure, which certifies agreement to six figures, S-wave penetration, P-wave exclusion, and alpha^5 leading dependence. It closes the numerical verification step of the QFT-012 derivation that obtains the Lamb shift from vacuum J-cost fluctuations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.