f_gap_def
plain-language theorem explainer
The lemma equates the master gap generator f_gap to the explicit logarithm of one plus the reciprocal of the golden ratio. Developers of the alpha prediction pipeline cite this identity when substituting the abstract F(1) into curvature corrections. The proof is a direct reflexivity step confirming the definitional match.
Claim. $f_ {gap} = {ln} (1 + {phi}^{-1})$ where {phi} is the golden ratio and f_gap is the generator at z=1 in the gap series.
background
In the Pipelines module the GapSeries namespace defines the master gap value as the generator at z=1 via the partial sum function F. The golden ratio phi is introduced as the concrete real number satisfying the self-similar fixed-point relation from the forcing chain. Upstream results supply the gap weight as w8 times log phi from the eight-tick DFT-8 projection and the voxel as the fundamental length quantum set to 1.
proof idea
The proof is a one-line term proof that applies reflexivity to equate the definition f_gap := F 1 with the closed-form expression Real.log (1 + 1 / phi).
why it matters
This equality supplies the explicit form of the gap weight required for the curvature-closure constant delta_kappa in the alpha pipeline. It feeds the higher-order alpha correction by replacing the abstract generator with the log expression derived from the eight-tick octave. The result supports the alpha inverse prediction band inside the Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.