lambShiftProofs
plain-language theorem explainer
This definition assembles a structured record of five Lamb shift properties derived from vacuum J-cost fluctuations, including the 1057-1059 MHz range and leading alpha^5 dependence. A physicist testing QED predictions or Recognition Science derivations would cite it to confirm numerical and structural agreement with the 1947 experiment. The construction is a direct record assignment that pulls each field from an independent upstream lemma or reflexivity.
Claim. The Lamb shift satisfies $1057 < lambShift_MHz < 1059$, the s-wave orbital angular momentum equals zero, the p-wave orbital angular momentum is positive, theoretical and experimental values agree to at least six significant figures, and the leading power of the fine-structure constant in the formula is five.
background
The module treats the Lamb shift as a QED effect arising from vacuum fluctuations reinterpreted as ledger J-cost fluctuations. Electron position uncertainty driven by these fluctuations modifies orbital J-cost and lifts the degeneracy between 2S_{1/2} and 2P_{1/2} levels. The structure LambShiftProofs collects the five required claims: numerical range, s-wave penetration, p-wave exclusion, six-figure precision, and alpha^5 scaling. Upstream lemmas supply the range via direct norm_num evaluation, the alpha power by reflexivity, and the angular-momentum statements by unfolding the centrifugal barrier definition.
proof idea
The definition is a one-line record constructor. It assigns the shift range field to the lamb_shift_approx theorem, the s-wave field to reflexivity, the p-wave field to the centrifugal-barrier exclusion theorem, the precision field to the six-figure agreement theorem, and the alpha-power field to the fifth-power theorem.
why it matters
This definition supplies the single reference object for all Lamb-shift claims in the QFT module, closing the local derivation from J-cost vacuum fluctuations. It directly implements the module target of reproducing the 1057 MHz splitting and the alpha^5 dependence required by the Recognition Science forcing chain. No downstream uses are recorded, leaving open its later embedding into a full QED consistency theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.