theory_more_precise
plain-language theorem explainer
The theorem asserts that the theoretical uncertainty on the Lamb shift is smaller than the experimental uncertainty, showing the Recognition Science J-cost model yields tighter bounds than current measurements. Precision QED spectroscopists would cite it when benchmarking vacuum-fluctuation predictions against data. The proof is a one-line term reduction that unfolds the two rational constants and applies norm_num to verify the inequality.
Claim. Let $0.0010$ MHz be the theoretical uncertainty and $0.0029$ MHz the experimental uncertainty on the Lamb shift. Then the theoretical uncertainty is strictly smaller: $0.0010 < 0.0029$.
background
The module derives the Lamb shift from vacuum J-cost fluctuations in the Recognition Science ledger, where electron jiggle arises from position uncertainty driven by the J-cost functional equation. Experimental uncertainty is defined as the rational 29/10000 MHz; theoretical uncertainty is the rational 10/10000 MHz. These constants sit inside the broader QFT-012 development that replaces standard QED vacuum polarization with ledger J-cost modifications to orbital energies.
proof idea
The term proof unfolds theoretical_uncertainty and experimental_uncertainty to expose their rational literals, then invokes norm_num to reduce the comparison 10/10000 < 29/10000 to a decidable numerical fact.
why it matters
The result strengthens the Recognition Science claim that the Lamb shift follows from J-cost vacuum fluctuations by establishing superior precision relative to experiment. It directly supports the module's target of reproducing the 1057 MHz splitting from the phi-ladder and RCL without invoking standard QED loops. No downstream theorems yet depend on it, leaving open its use in larger precision-QED chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.