three_point_affine_log_closure
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.
claimSuppose $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 in Recognition Science
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.
scope and limits
- Does not establish that the affine-log form is the only possible gap function arising from T0-T8.
- Does not provide numerical verification of the collapse for specific Z values.
- Does not extend the closure to non-integer arguments beyond the real definition.
- Does not address higher-order corrections or other candidate families.
formal statement (Lean)
236theorem three_point_affine_log_closure
237 {a b c : ℝ}
238 (hb : 1 < b)
239 (h0 : gapAffineLogR a b c 0 = 0)
240 (h1 : gapAffineLogR a b c 1 = 1)
241 (hneg1 : gapAffineLogR a b c (-1) = -2) :
242 ThreePointAffineLogClosure (a := a) (b := b) (c := c) := by
proof body
Term-mode proof.
243 have hparams : b = phi ∧ a = 1 / Real.log phi ∧ c = 0 :=
244 affine_log_parameters_forced_by_three_point_calibration hb h0 h1 hneg1
245 refine ⟨hparams.1, hparams.2.1, hparams.2.2, ?_⟩
246 exact affine_log_collapses_from_three_point_calibration hb h0 h1 hneg1
247
248end
249end GapFunctionForcing
250end Masses
251end IndisputableMonolith