gapAffineLog
plain-language theorem explainer
The declaration supplies the integer specialization of the affine-log gap candidate. Mass-ladder calculations in Recognition Science cite it when the gap must act on integer sector or charge values drawn from the anchor map. The definition is a one-line wrapper that embeds the integer argument into the reals and delegates to the real affine-log expression.
Claim. For real parameters $a,b,c$ and integer $Z$, the gap function is $g(Z) = a log(1 + Z/b) + c$, with $Z$ embedded in the reals.
background
The module works inside the affine-log family $g(x) = a log(1 + x/b) + c$ proposed as a bridge from multiplicative J-costs to additive rung shifts on the phi-ladder. Three normalization conditions (g(0)=0, g(1)=1, g(-1)=-2 with b>1) are shown elsewhere to force b=phi, a=1/log phi and c=0, collapsing the family to the canonical gap log_phi(1 + Z/phi). Upstream, the real-valued version is defined directly by that expression; the integer Z is the anchor map that converts rational charges into integers for lepton and quark sectors.
proof idea
One-line wrapper that casts the integer Z to a real and applies the real affine-log function.
why it matters
It supplies the integer version required by the collapse theorems affine_log_collapses_from_three_point_calibration and affine_log_collapses_to_canonical_gap. Those results close the three-point calibration that forces the canonical gap inside the affine-log family. The module documentation notes that the choice of this family itself remains a structural postulate motivated by the logarithmic cost-to-rung conversion rather than a derivation from the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.