three_point_affine_log_closure
plain-language theorem explainer
The declaration shows that three-point normalization conditions on the affine-log gap candidate force its parameters to the canonical Recognition Science form. Researchers deriving mass spectra from the phi-ladder would reference this result to justify the collapse of the candidate family. The proof proceeds by first extracting the forced coefficients via a dedicated lemma and then invoking the direct collapse statement.
Claim. Suppose $g(x) := a log(1 + x/b) + c$ with $b > 1$. Given the conditions $g(0) = 0$, $g(1) = 1$, $g(-1) = -2$, it follows that $b = phi$, $a = 1 / log phi$, $c = 0$, and $g(n)$ equals the canonical gap function for every integer $n$.
background
The module develops closure properties for the affine-log family $g(x) = a log(1 + x/b) + c$ under normalization. The definition gapAffineLogR implements this family on the reals, with an integer specialization gapAffineLog. The structure ThreePointAffineLogClosure packages the conclusions: the shift b is forced to phi, the scale a to 1 over log phi, the offset c to zero, and the function collapses to the RS gap on integers.
proof idea
The term proof begins by applying affine_log_parameters_forced_by_three_point_calibration to the hypotheses, yielding the equalities b = phi, a = 1 / Real.log phi, and c = 0. It then constructs the structure ThreePointAffineLogClosure by supplying these equalities together with the collapse statement obtained from affine_log_collapses_from_three_point_calibration.
why it matters
This theorem completes the three-point closure for the affine-log candidate, confirming that the normalizations eliminate all free parameters and recover the canonical gap function gap(Z) = log(1 + Z/phi) / log(phi). It supports the mass formula on the phi-ladder by fixing the gap function used in rung calculations. The result aligns with the eight-tick octave and D=3 landmarks by ensuring the gap is uniquely determined once the family is adopted, though the module notes that uniqueness of the family itself from T0-T8 remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.