IndisputableMonolith.RSBridge.GapProperties
The GapProperties module extends the gap function to real arguments to support concavity statements in the RS bridge to particle physics. Researchers deriving forced lepton masses cite these analytic properties. The module assembles separate lemmas on monotonicity, concavity, and increment behavior of the real extension.
claimThe real extension of the gap function $g(x) = {ln(1 + x/φ)}/{ln φ}$ satisfies $g(0) = 0$, is strictly increasing on $[0, ∞)$, and is strictly concave on $[0, ∞)$.
background
The Anchor module defines the gap function as the display function $F(Z) = {ln(1 + Z/φ)}/{ln φ}$ for the integer Z-map of the 12 fermions. Constants fixes the RS time quantum at one tick. GapProperties extends the function to reals specifically to enable concavity arguments required by mass derivations.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
Supplies the monotonicity and concavity lemmas required by the T9 electron mass necessity theorem and the T10 lepton generations necessity theorem. These close the step from the discrete Z-map to continuous arguments in the recognition framework.
scope and limits
- Does not derive any mass values.
- Does not address quarks or neutrinos.
- Does not invoke the T0-T8 forcing chain.
- Does not extend the domain past the reals.
used by (2)
depends on (2)
declarations in this module (20)
-
theorem
gap_zero -
theorem
gap_eq_log_phi_add_sub_one -
theorem
gap_strictMono_on_nonneg -
theorem
gap_24_lt_gap_276 -
theorem
gap_276_lt_gap_1332 -
def
gapR -
theorem
gapR_nat -
theorem
strictConcaveOn_gapR_Ici -
theorem
gap_diminishing_increments -
theorem
gap_second_difference_neg -
lemma
phi_bounds -
def
log_lower_bound_phi_hypothesis -
def
log_upper_bound_phi_hypothesis -
lemma
log_phi_bounds -
def
log_15p83_lower_hypothesis -
def
log_15p83_upper_hypothesis -
def
log_171p6_lower_hypothesis -
def
log_171p6_upper_hypothesis -
lemma
gap_24_bounds -
lemma
gap_276_bounds