lambShift
plain-language theorem explainer
The declaration assigns the Lamb shift frequency the value 1057.845 MHz inside the Recognition Science treatment of vacuum fluctuations. A QED or atomic-physics researcher would cite it when mapping the measured 2S-2P splitting in hydrogen onto the J-cost induced by discrete-time ledger fluctuations. The definition is a direct numerical constant whose justification is supplied by the surrounding module comment on electron-vacuum interaction.
Claim. The Lamb shift is the frequency splitting defined by $Δν := 1057.845$ MHz that arises when vacuum fluctuations modify the effective J-cost of the electron in the hydrogen atom.
background
The QFT.VacuumFluctuations module derives vacuum activity from τ₀ discreteness: time steps at the fundamental scale force energy fluctuations via the uncertainty relation, producing virtual pairs and zero-point energy. J-cost is the cost of a recognition event, given by the derived cost of a multiplicative recognizer’s comparator on positive ratios (MultiplicativeRecognizerL4.cost) or equivalently by Cost.Jcost on the state of a RecognitionEvent (ObserverForcing.cost). The module therefore treats the Lamb shift as the observable consequence of an electron interacting with these ledger fluctuations.
proof idea
The declaration is a one-line numerical definition. It receives its physical content from the immediately preceding module comment that identifies the shift with J-cost arising from vacuum-ledger fluctuations; no further lemmas or tactics are applied.
why it matters
The definition embeds the classic Lamb-shift datum inside the Recognition Science account of vacuum fluctuations generated by τ₀ discreteness. It thereby supplies a concrete numerical anchor for the QFT-010 program that traces zero-point energy to the eight-tick octave and J-uniqueness. Although the declaration is not yet referenced downstream, it supports the broader claim that the same discreteness mechanism addresses the cosmological-constant problem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.