alpha_fifth_power
plain-language theorem explainer
The declaration establishes that the leading power of the fine-structure constant in the Lamb shift energy formula is five. Researchers assembling Recognition Science derivations of QED effects or checking scaling in precision spectroscopy would cite it when confirming the alpha dependence of the shift. The proof is a one-line reflexivity that follows immediately from the definition of alpha_power_in_formula.
Claim. The leading term of the Lamb shift energy difference scales as the fifth power of the fine-structure constant: the exponent of $alpha$ in $Delta E sim alpha^5 m c^2 [ln(1/alpha) + cdots]$ is exactly 5.
background
In the Recognition Science treatment of QFT the Lamb shift is obtained from vacuum J-cost fluctuations that induce an effective position uncertainty for the electron and thereby modify its orbital J-cost. The module QFT.LambShift encodes the standard QED scaling through the definition alpha_power_in_formula, which is set to the numeral 5 so that the leading term matches the known $alpha^5$ dependence. Upstream results on ledger edge lengths and empirical programs supply the J-cost ledger that replaces conventional vacuum polarization in the derivation.
proof idea
The proof is a one-line reflexivity that matches the definition of alpha_power_in_formula directly to the numeral 5.
why it matters
This supplies the alpha_power field inside the LambShiftProofs structure that assembles the full RS derivation of the Lamb shift. It directly implements the power stated in the module doc-comment and confirms that the fifth power accounts for the smallness of the observed shift, consistent with the alpha band of the Recognition framework. No open scaffolding remains for this identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.