s_higher_than_p_by_lamb_shift
plain-language theorem explainer
The theorem establishes that the Lamb shift energy difference is positive, confirming the 2S state lies above the 2P state in hydrogen. Physicists working on QED precision tests or Recognition Science derivations would reference it to link vacuum fluctuations to observed level splitting. The proof is a one-line wrapper that unfolds the definition of the energy difference and evaluates the numerical inequality directly.
Claim. The Lamb shift energy difference satisfies $44/10 > 0$ in micro-electronvolts, raising the $2S_{1/2}$ level above the $2P_{1/2}$ level.
background
The module derives the Lamb shift from vacuum J-cost fluctuations in Recognition Science. Vacuum fluctuations equal ledger J-cost fluctuations, the electron jiggle equals J-cost-driven position uncertainty, and the level shift equals modification of orbital J-cost. The Lamb shift is the observed splitting between the 2S and 2P levels of hydrogen, absent in non-QED treatments but measured at roughly 1057 MHz.
proof idea
The proof is a one-line wrapper that unfolds the definition of lamb_shift_ueV to the constant 44/10 and applies norm_num to discharge the inequality.
why it matters
This result anchors the sign of the splitting inside the QFT-012 derivation of the Lamb shift from J-cost fluctuations. It aligns with the 1947 experimental discovery and the RS mechanism in which the 2S wave penetrates the nucleus and experiences a larger vacuum-induced shift. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.