s_wave_penetrates_nucleus
plain-language theorem explainer
When the angular momentum quantum number is zero the radial wavefunction reaches the origin. Recognition Science models of the Lamb shift cite this to justify why only S-states feel vacuum J-cost fluctuations at r=0. The proof is a one-line term that directly exhibits the positive rational witness 1.
Claim. If the orbital angular momentum quantum number satisfies $l=0$, then there exists a positive rational constant $c$ such that the S-wave amplitude at the nuclear origin is nonzero.
background
The module QFT.LambShift derives the 2S-2P splitting from vacuum J-cost fluctuations that modify orbital energy. The S-wave is introduced by the definition s_wave_l := 0. Upstream results supply the constant admissible path constructor from Action.PathSpace and the axiom-to-structure map from PrimitiveDistinction.from that underpins all Recognition Science derivations.
proof idea
Term-mode proof. The intro tactic consumes the hypothesis s_wave_l = 0; the exact tactic supplies the witness pair (1, norm_num) that satisfies the existential.
why it matters
The declaration closes the l=0 case required for the RS Lamb-shift mechanism in which only penetrating S-states couple to nuclear J-cost fluctuations. It sits inside the QFT-012 derivation before any numerical shift formula is assembled. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.