module module

`IndisputableMonolith.Masses.QuarkVerification`

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

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Masses.Anchor module_import
IndisputableMonolith.Masses.Verification module_import

declarations in this module (17)

def m_u_exp L47
def m_d_exp L48
def m_s_exp L49
def m_c_exp L50
def m_b_exp L51
def m_t_exp L52
theorem r_up_values L56
theorem r_down_values L61
theorem upquark_sector_params L76
theorem downquark_sector_params L80
theorem quark_mass_positive L89
theorem up_generation_spacing L107
theorem down_generation_spacing L113
theorem up_charm_to_up_ratio L127
theorem top_to_up_ratio L141
structure QuarkVerificationCert L157
theorem quark_verification_cert_exists L164