ThreePointAffineLogClosure
plain-language theorem explainer
The structure certifies that any affine-log gap function normalized at zero, one, and minus one must adopt shift equal to the golden ratio, scale equal to the reciprocal of its logarithm, and zero offset, collapsing exactly onto the canonical gap. Mass-spectrum calculations in Recognition Science cite it to confirm elimination of free parameters under three-point calibration. It is assembled directly as a record of the forced coefficients together with the resulting pointwise identity.
Claim. Let $a,b,c$ be real numbers and let $g(Z)=a log(1+Z/b)+c$ denote the affine-log family. The structure asserts $b=phi$, $a=1/log phi$, $c=0$, and $g(Z)$ equals the canonical gap function $log(1+Z/phi)/log phi$ for every integer $Z$.
background
The affine-log family is the candidate form $g(x)=a log(1+x/b)+c$ whose integer specialization is gapAffineLog. The canonical gap is the RSBridge display function $F(Z)=ln(1+Z/phi)/ln phi$, obtained as the closed-form residue at the anchor scale. Upstream, Gap45.Derivation.gap is the product of closure and Fibonacci factors whose main theorem states the gap equals 45, while PrimitiveDistinction.from extracts four structural conditions plus three definitional facts from seven independent axioms. The module records how three-point normalization removes all coefficient freedom once the family is adopted.
proof idea
The declaration is the structure definition itself. It directly records the three forced parameter equalities together with the pointwise identity to the canonical gap, without invoking additional lemmas or tactics.
why it matters
This certificate closes the affine-log family under three-point calibration and feeds directly into the downstream theorem three_point_affine_log_closure that constructs the certificate from the normalization hypotheses. It advances the Tier 1.1 step in Gap Function Forcing by removing free parameters, consistent with the phi-ladder and the eight-tick octave of the forcing chain. It leaves open 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.