IndisputableMonolith.Masses.GapFunctionForcing
The GapFunctionForcing module defines the affine-log family of candidate gap functions on the reals as a smooth extension of the discrete Z-map. Researchers deriving fermion masses from the phi-ladder would cite these definitions when calibrating against known particle data. The module consists of a sequence of definitions for gapAffineLogR and gapAffineLog together with lemmas that force the parameters via three-point calibration and normalizations.
claimThe affine-log gap function takes the form $g(r) = a log r + b$ for real $r > 0$, where the constants $a, b$ are uniquely determined by the normalizations $g(1) = 0$, $g(phi) = 1$, and a third calibration point from the Z-map, causing $g$ to coincide with the canonical gap $ln(1 + Z/phi)/ln phi$.
background
This module belongs to the Masses domain and imports the RS time quantum tau_0 = 1 from Constants together with the RSBridge.Anchor definitions of the 12 Standard Model fermions, the charge index Z_i = qtilde^2 + qtilde^4 (+4 for quarks), and the canonical gap F(Z) = ln(1 + Z/phi)/ln phi. The affine-log family is introduced as a real-valued candidate that can be calibrated to the discrete anchor points. Supporting identities include phi = 1 + 1/phi and its logarithm, which appear in the forcing lemmas.
proof idea
This is a definition module with supporting lemmas. It first records the basic phi identities phi_eq_one_add_inv_phi, one_add_inv_phi_eq_phi, and log_one_add_inv_phi_eq_log_phi. It then defines gapAffineLogR and gapAffineLog, followed by the forcing lemmas zero_normalization_forces_offset, unit_step_forces_log_scale, minus_one_step_forces_phi_shift, and affine_log_parameters_forced_by_three_point_calibration. The argument concludes with the collapse lemmas affine_log_collapses_to_canonical_gap and affine_log_unique_under_normalizations.
why it matters in Recognition Science
The module supplies the candidate gap family that links the discrete Z-map of the Anchor module to the continuous phi-ladder required for the mass formula yardstick * phi^(rung - 8 + gap(Z)). It shows that the affine-log form is the unique solution compatible with the three-point calibration and the Recognition Composition Law, thereby supporting the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain. The constructions prepare the ground for massAtAnchor evaluations in the broader masses domain.
scope and limits
- Does not compute numerical masses for any Standard Model particle.
- Does not extend the gap function beyond real arguments.
- Does not incorporate running couplings or quantum corrections.
- Does not address the Berry creation threshold at phi inverse.
- Does not derive the full mass spectrum without the phi-ladder assumptions.
depends on (2)
declarations in this module (14)
-
def
gapAffineLogR -
def
gapAffineLog -
lemma
phi_eq_one_add_inv_phi -
lemma
one_add_inv_phi_eq_phi -
lemma
log_one_add_inv_phi_eq_log_phi -
lemma
zero_normalization_forces_offset -
lemma
unit_step_forces_log_scale -
lemma
minus_one_step_forces_phi_shift -
theorem
affine_log_parameters_forced_by_three_point_calibration -
theorem
affine_log_collapses_to_canonical_gap -
theorem
affine_log_collapses_from_three_point_calibration -
theorem
affine_log_unique_under_normalizations -
structure
ThreePointAffineLogClosure -
theorem
three_point_affine_log_closure