ThreePointAffineLogClosure
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the affine-log family is the only possible gap function.
- Does not derive the form from the T0-T8 axioms.
- Does not compute explicit mass values or compare to data.
- Does not address renormalization flow beyond the anchor scale.
formal statement (Lean)
229structure ThreePointAffineLogClosure (a b c : ℝ) where
230 shift_forced : b = phi
231 scale_forced : a = 1 / Real.log phi
232 offset_forced : c = 0
233 collapses_to_gap : ∀ Z : ℤ, gapAffineLog a b c Z = RSBridge.gap Z
234
235/-- Build the closure certificate from three-point calibration data. -/