module module high

`IndisputableMonolith.RSBridge.GapProperties`

The GapProperties module extends the gap display function to real arguments and establishes its monotonicity, concavity, and increment properties. Researchers deriving forced lepton masses from the recognition framework cite these results when closing the T9 and T10 necessity arguments. The content consists of direct algebraic identities and applications of standard real-analysis facts from Mathlib.

claimThe real extension of the display function is $F(x) = \frac{\ln(1 + x/\phi)}{\ln\phi}$ for $x \in \mathbb{R}$, satisfying $F(0)=0$, strict monotonicity on $[0,\infty)$, and strict concavity on $[0,\infty)$.

background

The module sits inside the RSBridge layer and imports the gap definition from Anchor, where gap(F) is the display function $F(Z) = \ln(1 + Z/\phi)/\ln\phi$ that maps the charge index $Z_i = \tilde{q}^2 + \tilde{q}^4$ (+4 for quarks) to a logarithmic rung on the phi-ladder. Constants supplies the base time quantum $\tau_0 = 1$ tick. The real extension is introduced precisely to support concavity statements required by later mass-necessity proofs.

proof idea

This is a properties module establishing lemmas such as gap_zero, gap_eq_log_phi_add_sub_one, strictConcaveOn_gapR_Ici, gap_diminishing_increments, and gap_second_difference_neg through direct algebraic reduction and Mathlib real-analysis tactics.

why it matters in Recognition Science

Supplies the analytic properties of the gap function required by the T9 electron-mass necessity theorem in Physics.ElectronMass.Necessity and the T10 lepton-ladder necessity theorem in Physics.LeptonGenerations.Necessity. These downstream modules replace earlier axioms with inequalities derived from the gap concavity and increment lemmas.

scope and limits

Does not derive explicit fermion mass values.
Does not address the forcing chain from T0 through T8.
Does not perform numerical comparison with experimental data.
Does not treat complex or negative arguments beyond the stated domain.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.ElectronMass.Necessity module_import
IndisputableMonolith.Physics.LeptonGenerations.Necessity module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.RSBridge.Anchor module_import

declarations in this module (20)

theorem gap_zero L29
theorem gap_eq_log_phi_add_sub_one L39
theorem gap_strictMono_on_nonneg L65
theorem gap_24_lt_gap_276 L89
theorem gap_276_lt_gap_1332 L95
def gapR L103
theorem gapR_nat L106
theorem strictConcaveOn_gapR_Ici L110
theorem gap_diminishing_increments L194
theorem gap_second_difference_neg L264
lemma phi_bounds L292
def log_lower_bound_phi_hypothesis L320
def log_upper_bound_phi_hypothesis L323
lemma log_phi_bounds L326
def log_15p83_lower_hypothesis L346
def log_15p83_upper_hypothesis L349
def log_171p6_lower_hypothesis L352
def log_171p6_upper_hypothesis L355
lemma gap_24_bounds L358
lemma gap_276_bounds L406