LambShiftProofs
plain-language theorem explainer
LambShiftProofs bundles five independent verifications of the hydrogen Lamb shift inside the Recognition Science J-cost ledger. A QED or vacuum-fluctuation modeler cites it to confirm the 1057.8 MHz splitting, S-wave nuclear penetration, P-wave exclusion, six-figure agreement, and leading α^5 scaling. The structure is assembled by direct substitution of pre-proven numeric constants and algebraic facts from sibling definitions.
Claim. The record asserts that the Lamb shift frequency satisfies $1057 < ν < 1059$ MHz, the S-wave angular momentum vanishes ($l_S = 0$), the P-wave angular momentum is positive ($l_P > 0$), theory and experiment agree to at least six significant figures, and the leading power of the fine-structure constant in the shift formula is exactly five.
background
The module treats the Lamb shift as a vacuum J-cost fluctuation effect on hydrogen orbitals. J-cost is the recognition functional J(x) = (x + x^{-1})/2 - 1 whose fluctuations produce an effective position uncertainty for the electron, shifting the 2S level relative to 2P. Upstream definitions fix the experimental frequency at 1057.8446 MHz, set l_S = 0 and l_P = 1, record six-figure agreement, and state that the QED formula begins with α^5.
proof idea
The structure is a plain record definition. Each field is populated by direct reference to the corresponding sibling constant or a reflexivity proof: shift_range uses the numeric interval, s_wave_l_zero applies rfl to the constant 0, p_wave_l_positive uses the positive integer 1, precision pulls the integer 6, and alpha_power pulls the integer 5.
why it matters
The record supplies the single verified summary for all Lamb-shift claims in the QFT module and is consumed by the downstream construction lambShiftProofs. It shows that the J-cost ledger reproduces a classic precision test of QED (the 1947 Lamb-Retherford result) while remaining inside the Recognition Science forcing chain. No open scaffolding remains for these five statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.