Masses Gap Function Forcing

Gap Function Forcing

In Recognition Science, the mass ladder (the sequence of allowed particle masses) is described by a gap function that gives the multiplicative step between rungs. Masses gap function forcing is the result that, within a natural candidate family, this step function is uniquely determined by three calibration points. The candidate family is the affine-log form g(x) = a·log(1 + x/b) + c, where a, b, and c are real parameters.

The forcing works in two stages. First, with the shift parameter fixed at the golden ratio φ, the normalizations g(0)=0 and g(1)=1 force the offset c to zero and the scale a to 1/log φ. Second, adding a backward-step calibration g(-1)=-2 with the positive-shift branch b > 1 forces the shift itself: b = φ. The module proves these lemmas and packages them into the theorem affine_log_parameters_forced_by_three_point_calibration, which states that all three parameters are forced simultaneously.

The consequence is a collapse of the whole family to a single canonical gap: gap(Z) = log(1 + Z/φ) / log(φ), for integer rung index Z. The module proves this collapse in two forms: one assuming the shift is already known, and one deriving it from the three-point calibration. It also proves uniqueness: any two parameter sets satisfying the normalizations give the same gap on all integers. A compact certificate structure, ThreePointAffineLogClosure, records the forced parameters and the collapse in one object.

This is a closure step, not a derivation of the family itself. The affine-log family is adopted as a candidate; the forcing removes coefficient freedom once that family is chosen. The module does not prove that the family is uniquely forced from the deeper T0–T8 chain. That remains open.

THEOREM zero_normalization_forces_offset · unit_step_forces_log_scale · IndisputableMonolith/Masses/GapFunctionForcing.lean

THEOREM minus_one_step_forces_phi_shift · IndisputableMonolith/Masses/GapFunctionForcing.lean

THEOREM affine_log_parameters_forced_by_three_point_calibration · IndisputableMonolith/Masses/GapFunctionForcing.lean

THEOREM affine_log_collapses_from_three_point_calibration · IndisputableMonolith/Masses/GapFunctionForcing.lean

THEOREM affine_log_unique_under_normalizations · IndisputableMonolith/Masses/GapFunctionForcing.lean

What this page does not claim

This answer does not claim that the affine-log family is uniquely forced from T0–T8. This answer does not claim that the gap function has been derived from the ledger or recognition cost directly. This answer does not claim any empirical match between the canonical gap and measured masses.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/GapFunctionForcing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: