gapAffineLogR
plain-language theorem explainer
The affine-log candidate family on the reals is introduced as the parametric form g(x) = a log(1 + x/b) + c. Researchers deriving the canonical gap function via three-point calibration cite this definition as the starting family before normalization conditions are imposed. It is supplied as a direct one-line algebraic expression with no lemmas or tactics applied.
Claim. Define the real-valued function $g(a,b,c,x) = a log(1 + x/b) + c$ for parameters $a,b,c,x in mathbb{R}$.
background
The module GapFunctionForcing works inside the affine-log candidate family $g(x) = a cdot log(1 + x/b) + c$. Three normalization conditions fix the parameters: $g(0) = 0$ forces $c = 0$, $g(-1) = -2$ with $b > 1$ forces $b = phi$, and $g(1) = 1$ forces $a = 1/log(phi)$. The resulting canonical gap is $gap(Z) = log_phi(1 + Z/phi)$. This real-valued definition precedes the integer specialization gapAffineLog and supplies the parametric object on which the calibration theorems operate.
proof idea
This is a one-line definition that directly implements the expression $a * Real.log (1 + x / b) + c$.
why it matters
The definition supplies the parametric family whose uniqueness under the three normalizations is proved in affine_log_collapses_from_three_point_calibration and affine_log_collapses_to_canonical_gap. It therefore feeds every downstream result that converts the family into the canonical RS gap function on integers. The module doc states that the choice of the affine-log family itself remains a structural postulate motivated by the logarithmic cost-to-rung conversion rather than a theorem derived from T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.