lamb_shift_tiny
plain-language theorem explainer
The theorem shows the Lamb shift fraction is smaller than one part in 100000 relative to the hydrogen binding energy. QED modelers and Recognition Science derivations cite it to bound vacuum fluctuation corrections. The proof is a one-line wrapper that unfolds the fraction definition and applies norm_num for the numerical check.
Claim. The Lamb shift fraction satisfies $f < 1/100000$, where $f$ is the ratio of the vacuum-induced level shift to the ground-state binding energy in the hydrogen atom.
background
The module derives the Lamb shift as a vacuum J-cost fluctuation effect in Recognition Science, with J-cost defined via the functional equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The Lamb shift appears as a small modification to orbital J-cost for s-states, which penetrate the nucleus. Upstream results supply the probability measure on the quantum ledger and the local radius for cellular-automaton neighborhoods that model the underlying ledger dynamics.
proof idea
The proof is a one-line wrapper. It unfolds the definition of lambShiftFraction, then invokes norm_num to evaluate the concrete numerical bound and discharge the inequality.
why it matters
The result closes the size estimate for the QFT-012 Lamb shift mechanism, confirming the correction remains perturbative as required by the eight-tick octave and phi-ladder structure. It supports downstream consistency checks between RS-native constants and observed QED precision tests, without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.