orbital_angular_momentum
plain-language theorem explainer
S-waves carry orbital angular momentum quantum number zero while P-waves carry one unit. Atomic physicists modeling the hydrogen Lamb shift cite this assignment when separating centrifugal barrier effects on vacuum J-cost fluctuations. The proof is a one-line wrapper that splits the conjunction and matches the two constant definitions by reflexivity.
Claim. $l_S = 0$ and $l_P = 1$, where $l_S$ is the orbital angular momentum quantum number assigned to S-waves and $l_P$ the value assigned to P-waves.
background
The QFT.LambShift module derives the 1057 MHz splitting between 2S and 2P hydrogen levels from ledger J-cost fluctuations in the vacuum. Orbital angular momentum enters through the centrifugal term that alters wavefunction penetration at the origin and therefore the local J-cost experienced by the electron. The sibling definitions fix s_wave_l to the natural number 0 and p_wave_l to the natural number 1.
proof idea
The proof is a one-line wrapper that applies the constructor tactic to split the conjunction and then uses reflexivity to match each side against the defining equations of s_wave_l and p_wave_l.
why it matters
The assignment supplies the angular-momentum distinction required for any subsequent Lamb-shift calculation that separates S-wave penetration from P-wave exclusion. It sits inside the RS treatment of vacuum fluctuations as J-cost variations and prepares the ground for the explicit frequency-shift formulas that follow in the same module. No open scaffolding remains; the values are taken as the standard spectroscopic labels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.