gap_minus_shift_bounds
plain-language theorem explainer
Bounds on the difference between gap at 1332 and the refined shift are established as lying strictly inside (-20.7063, -20.705). Electron mass derivations in Recognition Science cite this interval as a numerical check on the T9 ledger fraction residue. The proof obtains separate interval bounds from Necessity and combines them with linear arithmetic.
Claim. Let $g = $ gap$(1332)$ and let $s$ be the refined shift. Then $-20.7063 < g - s < -20.705$.
background
In Recognition Science the gap function is the anchor residue $g(Z) = $ ln$(1 + Z/φ) /$ ln$φ$, with $Z = 1332$ for the electron sector. The refined shift is the correction term appearing in the T9 residue formula $δ = 2W + (W + E_{total})/(4 E_{passive}) + α^2 + E_{total} α^3$ (W = 17, E_total = 12, E_passive = 11). The module derives the electron mass by showing that the observed residue matches gap minus this shift to the stated precision.
proof idea
The tactic proof first calls Necessity.gap_1332_bounds and Necessity.refined_shift_bounds to obtain the four endpoint inequalities. It then splits the target conjunction with constructor and discharges both sides by linarith on those four facts.
why it matters
The result is invoked inside electron_mass_ledger_hypothesis to bound the absolute difference between electron residue and (gap 1332 minus refined shift) by 0.002. It supplies the concrete numerical content for the T9 step of the forcing chain, confirming consistency with the phi-ladder and the alpha band (137.03, 137.039). Tighter matching to 10^{-6} remains open and would require stronger input bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.