module module

`IndisputableMonolith.RSBridge.GapProperties`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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