f_gap
plain-language theorem explainer
f_gap supplies the gap correction in the exponential formula for the inverse fine-structure constant. Researchers deriving alpha from Recognition Science constants cite this definition to keep the pipeline parameter-free. It is a direct one-line definition that multiplies the closed-form eight-tick projection weight by the natural logarithm of the golden ratio.
Claim. $f_ {gap} := w_8 ln phi$, where $w_8$ is the normalized projection weight of the gap onto the fundamental 8-tick basis and $phi = (1 + sqrt{5})/2$ is the golden ratio.
background
In the GapWeight module the eight-tick octave supplies the gap weight via the closed-form expression w8_from_eight_tick = (348 + 210 sqrt{2} - (204 + 130 sqrt{2}) phi)/7. The module states that this is the normalized projection weight onto the 8-tick basis and that f_gap is obtained by multiplying it by ln phi. The local setting is the alpha pipeline, where a single gap term enters the exponential resummation for alpha inverse.
proof idea
This is a direct definition. It multiplies the parameter-free w8_from_eight_tick by Real.log phi.
why it matters
This definition supplies the gap input to alphaInv and to the derived alpha components in Constants.Alpha. It feeds the main theorems alphaInv_derived_eq_formula and curvature_term_eq in AlphaDerivation. In the framework it realizes the T7 eight-tick octave contribution to the constants while closing the no-free-parameters claim for the fine-structure constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.