f_gap
plain-language theorem explainer
The gap weight function takes a real scalar w8 from the eight-tick DFT-8 projection and returns w8 multiplied by the natural log of the golden ratio. Researchers assembling the Recognition Science derivation of the inverse fine-structure constant cite this term when forming the exponential resummation α^{-1} = α_seed exp(-f_gap/α_seed). The implementation is a direct one-line definition that substitutes φ = (1 + sqrt(5))/2.
Claim. $f_8(w_8) = w_8 ln φ$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module formalizes higher-order voxel-seam corrections to α^{-1} on the Q3 cube, with the series α^{-1} = α_seed − f_gap + Σ_{n=1}^∞ δ_n. The gap weight originates from the DFT-8 projection; the upstream GapWeight definition supplies the fixed master value as w8_from_eight_tick * log φ. A second upstream result defines the strictly positive φ-ladder correction 1/(φ N) for quantum channel capacity at positive input-symbol count N.
proof idea
One-line definition that multiplies the input weight w8 by Real.log of the locally introduced golden ratio φ = (1 + Real.sqrt 5)/2. No tactics or lemmas are applied beyond the direct substitution.
why it matters
This supplies the gap term required by alphaInv to define the canonical exponential form α^{-1} = α_seed * exp(−f_gap/α_seed) and by alpha_components_derived to witness the seed-gap pair. It implements the gap-weight ingredient of the RS derivation that targets the CODATA value 137.035999206(11) while leaving the explicit computation of the next-order δ2 term open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.