gapAffineLogR
plain-language theorem explainer
The affine-log candidate family on the reals is defined by the expression a times the natural logarithm of one plus x over b, plus c. Mass-gap researchers cite this as the explicit starting object for three-point calibration arguments that force the shift parameter b to equal phi. The definition is a direct one-line algebraic expression with no auxiliary lemmas or reductions.
Claim. The function $g(x) = a log(1 + x/b) + c$ for real parameters $a, b, c$ and variable $x$.
background
In the Gap Function Forcing module the affine-log family is introduced as a concrete candidate for the gap function inside Recognition Science. The module records how the normalizations g(0)=0 and g(1)=1 together with the backward calibration g(-1)=-2 collapse all free coefficients once b is fixed at phi, yielding the canonical form gap(Z) = log(1 + Z/phi)/log(phi). Upstream structures supply the necessary background: J-cost minimization (strict convexity of J(x) = (x + 1/x)/2 - 1) from PhysicsComplexityStructure, phi-forcing from PhiForcingDerived, and the discrete phi-tiers of nuclear densities from NucleosynthesisTiers.
proof idea
This is a definition implemented as the direct expression a * Real.log (1 + x / b) + c. No lemmas are invoked; the object is the base for all subsequent parameter-forcing theorems in the same module.
why it matters
The definition supplies the explicit family that downstream theorems (affine_log_collapses_from_three_point_calibration, affine_log_collapses_to_canonical_gap, affine_log_parameters_forced_by_three_point_calibration) collapse to the canonical RS gap. It executes the concrete closure step for Tier 1.1 described in the module doc, removing coefficient freedom once the affine-log form is adopted and linking directly to the phi-ladder and T5 J-uniqueness. It does not yet prove the family itself is forced from T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.