gap_correction_positive
plain-language theorem explainer
Positivity of the gap correction term in the exponential resummation formula for alpha inverse holds whenever the weight w and seed are positive reals. Fine structure constant precision work in Recognition Science cites this to keep the correction factor strictly positive inside the target band. The proof is a one-line term reduction that unfolds the definition and invokes multiplication positivity together with exponential positivity.
Claim. If $w>0$ and $s>0$, then $0 < s · exp(−(w ln ϕ)/s)$, where ϕ is the golden ratio and the expression is the gap correction factor in the resummation α⁻¹ = α_seed · exp(−w₈ ln ϕ / α_seed).
background
The Alpha-Inverse Precision Refinement module (Q8) supplies two formulas for α⁻¹: the additive seed 4π × 11 and the exponential resummation α_seed × exp(−w₈ ln ϕ / α_seed) with α_seed = 44π. The gap_correction function is defined exactly as seed · exp(−(w · log ϕ)/seed). Upstream ConstantDerivations supplies the related numerical gap factor 1 + 45/(360·137) that accounts for the D=3 integration gap of 45; MassLaw supplies the distinct rung correction log_ϕ(1 + Z/ϕ). The module states that α⁻¹ lies in (137.030, 137.039) with zero sorrys.
proof idea
The term proof unfolds gap_correction to the product seed · exp(−(w log ϕ)/seed), then applies the lemma mul_pos to the hypothesis 0 < seed and the fact that Real.exp_pos yields a positive exponential for any real argument.
why it matters
The result is invoked by alpha_precision_cert_exists to populate the gap_positive field of AlphaPrecisionCert, thereby certifying the 60 ppm interval for α⁻¹. It closes the positivity requirement for the exponential resummation step in the Q8 refinement that targets 1 ppm accuracy. Within the Recognition framework it preserves sign consistency of the correction on the phi-ladder, aligning with the eight-tick octave and the geometric seed construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.