p_wave_l
plain-language theorem explainer
The definition assigns the orbital angular momentum quantum number l=1 to P-waves in the Recognition Science treatment of the hydrogen Lamb shift. Researchers deriving QED-level corrections from vacuum J-cost fluctuations cite this assignment to separate S-state penetration from P-state exclusion at the origin. The declaration is a direct numerical assignment requiring no lemmas or computation.
Claim. The P-wave angular momentum quantum number satisfies $l_P = 1$.
background
The QFT.LambShift module derives the Lamb shift from vacuum J-cost fluctuations, where electron jiggle arises as position uncertainty driven by ledger J-cost and level shifts modify orbital J-cost. The upstream ILG action is defined as S[g, ψ; C_lag, α] := S_EH[g] + S_ψ[g,ψ], reducing to pure Einstein-Hilbert gravity when the lag and alpha parameters vanish. This definition supplies the P-wave value l=1 to contrast with the S-wave value l=0, enabling the centrifugal barrier analysis that excludes P-states from r=0.
proof idea
The declaration is a direct definition that assigns the constant 1. No lemmas are invoked and no tactics are applied beyond the built-in abbreviation expansion.
why it matters
This definition feeds the LambShiftProofs structure, which asserts the numerical Lamb shift range 1057-1059 MHz, s_wave_l=0, p_wave_l>0, six-significant-figure precision, and leading alpha^5 dependence. It completes the QFT-012 target of obtaining the Lamb shift from J-cost fluctuations and supports the orbital_angular_momentum theorem that simultaneously records l=0 for S-waves and l=1 for P-waves. The assignment is consistent with the Recognition Science eight-tick octave and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.