gap_correction
plain-language theorem explainer
The gap_correction definition supplies the multiplicative exponential factor in the resummation formula for the inverse fine structure constant. Precision calculations of α in Recognition Science cite this when establishing the interval (137.030, 137.039). It is a direct one-line definition of the term seed * exp(−(w * log phi)/seed) drawn from the module's exponential resummation.
Claim. The exponential gap correction is defined by $gap(w, s) := s · exp(−(w ln φ)/s)$, where $s$ denotes the geometric seed and $w$ the weight parameter in the fine-structure resummation.
background
The Alpha-Inverse Precision Refinement module computes α^{-1} from an additive seed α^{-1}_add = 4π × 11 ≈ 138.23 and the exponential form α^{-1} = α_seed × exp(−w_8 ln φ / α_seed) with α_seed = 44π and w_8 ≈ 2.490. This gap_correction implements the exponential multiplier. Upstream results include the gap-45 correction in ConstantDerivations, which accounts for the integration gap D²(D+2) = 45 at D = 3, and the charge-dependent gap in MassLaw given by log_φ(1 + Z/φ). The module reports that α^{-1} lies in (137.030, 137.039), about 60 ppm wide, with a target of 1 ppm requiring an additional curvature correction.
proof idea
This declaration is a direct definition that transcribes the exponential resummation formula α_seed × exp(−w ln φ / α_seed) into Lean code using Real.exp and Real.log applied to phi.
why it matters
It provides the exponential term required by the AlphaPrecisionCert structure to certify the precision bounds on α^{-1}. The definition supports the framework's constant derivations from the phi-ladder and the eight-tick octave at D = 3. It feeds into mass law applications indirectly through shared constant infrastructure. The remaining open question is the inclusion of the curvature correction δ_κ to reach 1 ppm accuracy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.