gapAffineLog
plain-language theorem explainer
gapAffineLog specializes the real affine-log gap family to integer arguments Z, enabling direct use on discrete charge or rung labels in mass calculations. Researchers deriving particle spectra from the Recognition framework cite it when applying three-point normalizations to collapse the candidate family. The definition is a one-line wrapper that casts Z to real and delegates to the underlying gapAffineLogR.
Claim. The integer specialization of the affine-log family is defined by $gapAffineLog(a, b, c, Z) := a · log(1 + Z/b) + c$ for real coefficients $a, b, c$ and integer $Z$.
background
The GapFunctionForcing module records concrete closure steps for Tier 1.1 within the candidate family $g(x) = a · log(1 + x/b) + c$. With fixed $b = φ$, the normalizations $g(0) = 0$ and $g(1) = 1$ force the canonical coefficients; adding the backward calibration $g(-1) = -2$ forces the shift $b = φ$ itself. The upstream gapAffineLogR supplies the real-valued definition $a · Real.log(1 + x/b) + c$. The integer version permits direct application to Z values arising from anchor relations in lepton and quark sectors.
proof idea
This definition is a one-line wrapper that applies gapAffineLogR after casting the integer Z to a real number.
why it matters
It provides the integer interface required by downstream results such as affine_log_collapses_to_canonical_gap and ThreePointAffineLogClosure, which prove equality to the canonical RS gap under the structural normalizations. The declaration fills the concrete closure step described in the module doc-comment, removing coefficient freedom once the affine-log family is adopted and linking to the phi-ladder mass formula. It touches the open question whether the affine-log form itself is uniquely forced from T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.