dirac_degeneracy
plain-language theorem explainer
Dirac theory equates the binding energies of the 2S and 2P hydrogen states at 3.4 eV each. Researchers deriving the Lamb shift from vacuum fluctuations cite this equality as the pre-QED degeneracy baseline. The definition directly equates the two energy constants with no additional computation.
Claim. Without QED corrections the binding energies of the 2S and 2P states in hydrogen satisfy $E_{2S} = E_{2P}$.
background
The module derives the Lamb shift from vacuum J-cost fluctuations, where vacuum fluctuations equal ledger J-cost fluctuations and level shifts arise from orbital J-cost modifications. The module states that without QED the 2S and 2P levels are degenerate. Upstream energy definitions both evaluate to 3.4 eV, while the ILG action supplies the relativistic context and decision theory supplies correlation predictions used elsewhere.
proof idea
This is a definition that directly sets the degeneracy proposition to the equality of the two energy constants. It is a one-line wrapper with no lemmas applied beyond the constant definitions.
why it matters
It supplies the degeneracy baseline for the downstream Dirac prediction theorem, which is proved by reflexivity. This anchors the pre-QED limit in the Lamb shift derivation before J-cost fluctuations lift the degeneracy. It corresponds to the classical Dirac theory step in the Recognition framework prior to vacuum ledger modifications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.