module module high

`IndisputableMonolith.RSBridge.GapProperties`

GapProperties extends the gap display function from integer Z to real arguments and proves its monotonicity, concavity, and diminishing-increment properties. Mass-ladder derivations in electron and lepton necessity proofs cite these results to justify continuous approximations. The module consists of direct algebraic lemmas and standard real-analysis arguments on the extended function.

claimThe real extension $F:\mathbb{R}\to\mathbb{R}$ of the gap function satisfies $F(0)=0$, is strictly increasing and strictly concave on $[0,\infty)$, obeys $F(x+1)-F(x)$ strictly decreasing, and meets the explicit bounds $F(24)<F(276)<F(1332)$.

background

The gap function is introduced in RSBridge.Anchor as the display function $F(Z)=\ln(1+Z/\phi)/\ln\phi$ that converts the charge-indexed integer $Z_i$ into a real rung on the phi-ladder. Constants supplies the underlying time quantum $\tau_0=1$ tick. GapProperties extends this $F$ from integers to reals precisely to support concavity statements required downstream.

proof idea

The module proves a chain of lemmas by direct substitution and differentiation: gap_zero and gap_eq_log_phi_add_sub_one establish the base value and logarithmic identity; gap_strictMono_on_nonneg and gapR_nat give monotonicity; gap_24_lt_gap_276 and gap_276_lt_gap_1332 supply concrete comparisons; strictConcaveOn_gapR_Ici and gap_second_difference_neg establish concavity via the second-difference test.

why it matters in Recognition Science

These analytic properties feed directly into ElectronMass.Necessity (T9) and LeptonGenerations.Necessity (T10), where they justify the inequalities that close the forcing chain from T8 ledger quantization to forced lepton masses. The module supplies the continuous bridge between the discrete Z-map of Anchor and the real-valued mass formulas needed for the necessity arguments.

scope and limits

Does not derive any particle mass values.
Does not treat negative real arguments.
Does not connect to quantum-field interpretations.
Does not replace the integer Z-map of Anchor.

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