relatedEffects
plain-language theorem explainer
This definition enumerates four other precision QED tests that share the vacuum J-cost fluctuation mechanism with the Lamb shift. A researcher deriving QED corrections from Recognition Science would cite it to group g-2, hyperfine splitting, positronium, and muonium spectroscopy under the same ledger framework. The definition is a direct static list with no computation or lemmas applied.
Claim. The related precision QED effects are the anomalous magnetic moment $(g-2)/2$ of the electron, the hyperfine splitting of hydrogen, positronium $(e^+e^-)$ spectroscopy, and muonium $(μ^+e^-)$ spectroscopy.
background
The QFT.LambShift module derives the Lamb shift from vacuum J-cost fluctuations, where electron position uncertainty arises from ledger J-cost minimization and modifies orbital energy levels. J-cost is defined as $J(x) = (x + x^{-1})/2 - 1$, the strictly convex function whose global minimum occurs at $x=1$. Upstream structures supply the necessary scaffolding: PhiForcingDerived.of gives the structure of J-cost, PhysicsComplexityStructure.of states that J-cost minimization is convex with local 8-tick dynamics, and SpectralEmergence.of forces the gauge content SU(3)×SU(2)×U(1) together with exactly three generations.
proof idea
The declaration is a direct definition that returns a fixed list of four strings. No tactics or lemmas are invoked; the body simply enumerates the effects named in the module doc-comment as other precision QED tests.
why it matters
The definition completes the narrative of the LambShift module by placing the derived Lamb shift alongside the standard precision QED observables that must also arise from J-cost fluctuations. It supports the Recognition Science program of obtaining all QED corrections from the single functional equation via T5 J-uniqueness and the Recognition Composition Law. No downstream theorems depend on it yet, leaving open the question of explicit derivations for g-2 and hyperfine splitting within the same ledger framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.