IndisputableMonolith.Masses.GapFunctionForcing
The GapFunctionForcing module defines the affine-log candidate family on the reals as a parameterized model for the gap function in Recognition Science mass derivations. Researchers calibrating fermion masses via the Z-map and phi-ladder would cite its normalization lemmas. The module structure consists of basic affine-log definitions followed by forcing lemmas that collapse the family to the canonical gap under three-point calibration.
claimThe affine-log family comprises functions of the form $g(x) = a + b log(c + d x)$ on the reals, calibrated so that $g(Z) = F(Z) = ln(1 + Z/φ)/ln(φ)$ at anchor points, with parameters forced by zero, unit-step, and minus-one normalizations.
background
This module sits in the Masses domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the core bridge from RSBridge.Anchor. The Anchor module defines Fermion (the 12 SM species), ZOf (charge-indexed integer Z_i = q̃² + q̃⁴ + 4 for quarks), the gap display function F(Z) = ln(1 + Z/φ)/ln(φ), and massAtAnchor at scale μ⋆. The affine-log family supplies a real-valued candidate that can be forced to reproduce F(Z).
proof idea
This is a definition module, no proofs. It introduces gapAffineLogR and gapAffineLog, records the elementary identities phi_eq_one_add_inv_phi and log_one_add_inv_phi_eq_log_phi, then states the normalization lemmas zero_normalization_forces_offset, unit_step_forces_log_scale, minus_one_step_forces_phi_shift, and the collapse results affine_log_collapses_to_canonical_gap and affine_log_unique_under_normalizations.
why it matters in Recognition Science
The module forces the gap function to its canonical log form, supplying the unique affine-log realization required by the mass formula yardstick * φ^(rung - 8 + gap(Z)). It thereby supports the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain while providing the concrete bridge from the Anchor module's F(Z) to the phi-ladder spectrum. No direct downstream declarations are recorded.
scope and limits
- Does not compute explicit numerical masses for any fermion.
- Does not extend the affine-log family beyond the real line.
- Does not invoke the Recognition Composition Law.
- Does not address the eight-tick octave or D = 3.
- Does not connect to the alpha band or Berry threshold.
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