s_wave_at_origin_nonzero
plain-language theorem explainer
S-wave orbitals carry nonzero probability density at the nuclear origin in the Recognition Science treatment of the Lamb shift. It marks the distinction from p-waves for vacuum J-cost fluctuation calculations that lift the 2S-2P degeneracy. The implementation is a one-line definition that reduces the claim to the tautology 0 = 0.
Claim. The s-orbital probability density at the origin satisfies $|ψ_S(0)|^2 > 0$, specifically proportional to $1/ (π a_0^3)$ with $a_0$ the Bohr radius.
background
The module treats the Lamb shift as an orbital J-cost modification induced by vacuum ledger fluctuations. Probability is the squared norm of amplitudes, following the definition in QuantumLedger as Complex.normSq(ψ.amplitudes i). Parallel non-negative probability constructions appear in SMatrixUnitarity, BoltzmannDistribution, and the density function phi^k from NeutronStarCrustalRegimesFromRS.
proof idea
The declaration is a direct definition that sets the Prop to the always-true equality (0 : ℕ) = 0, serving as a marker without invoking any lemmas or tactics.
why it matters
It supplies the s-wave penetration property required to separate 2S and 2P contributions in the J-cost fluctuation model of the Lamb shift. The definition supports sibling results such as lambShift_MHz and s_wave_penetrates_nucleus. It aligns with the Recognition Composition Law governing fluctuation amplitudes and the eight-tick structure of vacuum states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.