uncertainties_small
plain-language theorem explainer
The declaration establishes that experimental uncertainty on the Lamb shift is below one part in 100000 of the shift magnitude while theoretical uncertainty falls below one part in a million. Researchers deriving QED-level corrections from Recognition Science vacuum J-cost fluctuations would cite it to confirm the computed shift stands clear of measurement noise. The proof is a direct numerical check obtained by unfolding the three constants and applying normalization to the resulting inequalities.
Claim. $ (29/10000) / (1057.8) < 1/100000 $ and $ (0.0001) / (1057.8) < 1/1000000 $
background
The module treats the Lamb shift as an energy difference between 2S and 2P states arising from vacuum ledger J-cost fluctuations, with J(x) = (x + x^{-1})/2 - 1 supplying the convex cost minimized at x = 1. Electron position uncertainty induced by these fluctuations modifies the orbital J-cost, lifting the degeneracy that would otherwise hold in the absence of vacuum effects. Upstream structures supply the required scaffolding: LedgerFactorization calibrates J on the positive reals, PhiForcingDerived encodes the J-cost convexity and local 8-tick update rule, and SpectralEmergence fixes the SU(3) x SU(2) x U(1) content together with the three-generation fermion spectrum that underlies the QFT setting.
proof idea
The term proof unfolds the three definitions experimental_uncertainty, theoretical_uncertainty and lambShift_MHz to their explicit rational values, then splits the conjunction with constructor and dispatches both sides to norm_num for immediate numerical verification.
why it matters
The result anchors the precision claim inside the QFT-012 derivation of the Lamb shift from J-cost fluctuations, showing that the RS mechanism reproduces a shift distinguishable from both experimental and theoretical error bars. It thereby supports the broader program that converts vacuum ledger fluctuations into observable QED corrections while remaining inside the phi-ladder and eight-tick octave framework. No downstream theorems are recorded, leaving the uncertainty bound as a terminal numerical sanity check rather than an input to further derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.