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

f_gap

show as:
view Lean formalization →

The master gap value is obtained by evaluating the generating functional at unit argument. It enters the exponential resummation formula for the inverse fine-structure constant as the gap term in alpha derivations. The definition consists of a direct substitution into the logarithmic form F(z) = log(1 + z/φ) with φ the golden ratio.

claim$f_ {gap} := log(1 + 1/φ)$, where φ denotes the golden ratio and log is the natural logarithm.

background

The Pipelines module sets φ as a concrete real number and introduces the generating functional F(z) := log(1 + z/φ). This functional produces gap quantities for constant derivations. The upstream definition of F supplies the explicit logarithmic expression used here.

proof idea

The definition is a direct one-line substitution that evaluates the generating functional F at the argument 1.

why it matters in Recognition Science

This definition supplies the gap input required by the exponential form of alphaInv in Constants.Alpha and the derived expressions in AlphaDerivation. It closes the structural gap in the first-principles derivation of α^{-1} from the seed 4π·11 and the logarithmic gap. The construction ties into the Recognition Science use of φ in the eight-tick octave through the gap weight.

scope and limits

formal statement (Lean)

  30noncomputable def f_gap : ℝ := F 1

used by (40)

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

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.