f_gap
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.