refined_shift_bounds
plain-language theorem explainer
The lemma pins the refined shift for the electron to the interval (34.6590, 34.6593). Mass-spectrum calculations that place the electron on the phi-ladder cite this bound to close the gap-minus-shift step. The proof is a one-line wrapper that adds the already-proven base-shift interval to the radiative-correction interval and invokes linear arithmetic.
Claim. $34.6590 < b + r < 34.6593$, where $b$ is the base shift obtained from the exact ledger fraction and $r$ is the second-order radiative correction built from powers of the fine-structure constant.
background
Module T9 shows that the electron mass is forced once T8 ledger quantization and the geometric constants are fixed. The refined shift is defined as base_shift + radiative_correction. Base shift comes from the wallpaper-group ledger fraction; radiative correction assembles the alpha-squared and alpha-cubed terms that appear in the QFT expansion of the self-energy. The two upstream lemmas supply the separate numeric intervals that are added here.
proof idea
Term-mode proof. It unfolds the definition of refined_shift, pulls in the two prior bounds (base_shift_bounds and radiative_correction_bounds), then applies constructor followed by linarith to obtain the combined interval.
why it matters
This lemma supplies the shift half of the gap-minus-shift bounds used by both the electron-mass theorem and the lepton-generation necessity result. It therefore closes one numeric link in the T9 forcing chain that derives the electron mass from T8 and the phi-ladder. The parent theorems appear in Physics.ElectronMass and Physics.LeptonGenerations.Necessity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.