p_wave_excluded_from_origin
plain-language theorem explainer
P-waves carry positive orbital angular momentum, so their wavefunctions are excluded from the nuclear origin by the centrifugal barrier. Researchers deriving the Lamb shift from J-cost vacuum fluctuations cite this separation to isolate s-wave penetration effects. The proof is a one-line wrapper that unfolds the definition of the p-wave angular momentum quantum number and applies numerical normalization.
Claim. The orbital angular momentum quantum number for p-waves satisfies $l > 0$.
background
The module derives the Lamb shift as an energy difference between 2S and 2P hydrogen levels induced by vacuum J-cost fluctuations. P-waves are defined by the angular momentum quantum number equal to 1, while s-waves have zero. This rests on the ILG action that combines Einstein-Hilbert and psi-field terms, together with RS-native energy units and crystal structure classifications.
proof idea
The proof unfolds the definition of the p-wave angular momentum quantum number (set to 1) and applies norm_num to confirm the strict inequality.
why it matters
The result is recorded in the Lamb shift proof summary as the positive angular momentum fact that distinguishes p-states from s-states. It supports the RS claim that only l=0 components feel the full J-cost shift near the origin, consistent with the phi-ladder and eight-tick structure. It closes one step in the QFT-012 derivation without touching higher-order QED corrections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.