pith. machine review for the scientific record. sign in
def definition def or abbrev high

f_gap

show as:
view Lean formalization →

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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 114noncomputable def f_gap : ℝ := w8_from_eight_tick * Real.log phi

proof body

Definition body.

 115

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (3)

Lean names referenced from this declaration's body.